`∀[C:SmallCategory]. ∀[M:Monad(C)]. ∀[x:cat-ob(C)].`
`  ((((cat-comp(C) M(x) M(M(x)) M(x) monad-unit(M;M(x)) monad-op(M;x)) = (cat-id(C) M(x)) ∈ (cat-arrow(C) M(x) M(x)))`
`  ∧ ((cat-comp(C) M(x) M(M(x)) M(x) (monad-functor(M) x M(x) monad-unit(M;x)) monad-op(M;x))`
`    = (cat-id(C) M(x))`
`    ∈ (cat-arrow(C) M(x) M(x))))`
`  ∧ ((cat-comp(C) M(M(M(x))) M(M(x)) M(x) monad-op(M;M(x)) monad-op(M;x))`
`    = (cat-comp(C) M(M(M(x))) M(M(x)) M(x) (monad-functor(M) M(M(x)) M(x) monad-op(M;x)) monad-op(M;x))`
`    ∈ (cat-arrow(C) M(M(M(x))) M(x))))`

Proof

Definitions occuring in Statement :  monad-op: `monad-op(M;x)` monad-unit: `monad-unit(M;x)` monad-fun: `M(x)` monad-functor: `monad-functor(M)` cat-monad: `Monad(C)` functor-arrow: `arrow(F)` cat-comp: `cat-comp(C)` cat-id: `cat-id(C)` cat-arrow: `cat-arrow(C)` cat-ob: `cat-ob(C)` small-category: `SmallCategory` uall: `∀[x:A]. B[x]` and: `P ∧ Q` apply: `f a` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` cat-monad: `Monad(C)` spreadn: spread3 monad-fun: `M(x)` monad-op: `monad-op(M;x)` monad-unit: `monad-unit(M;x)` pi2: `snd(t)` pi1: `fst(t)` monad-functor: `monad-functor(M)` all: `∀x:A. B[x]`
Lemmas referenced :  cat-ob_wf cat-monad_wf small-category_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename productElimination sqequalRule hypothesis dependent_functionElimination hypothesisEquality independent_pairFormation because_Cache independent_pairEquality axiomEquality extract_by_obid isectElimination isect_memberEquality

Latex:
=  (cat-id(C)  M(x))))