`∀[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) (arrow(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) (arrow(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 :  all: `∀x:A. B[x]` monad-functor: `monad-functor(M)` pi1: `fst(t)` pi2: `snd(t)` monad-unit: `monad-unit(M;x)` monad-op: `monad-op(M;x)` monad-fun: `M(x)` spreadn: spread3 cat-monad: `Monad(C)` cand: `A c∧ B` and: `P ∧ Q` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  small-category_wf cat-monad_wf cat-ob_wf
Rules used in proof :  isect_memberEquality isectElimination extract_by_obid axiomEquality independent_pairEquality because_Cache independent_pairFormation hypothesisEquality dependent_functionElimination hypothesis sqequalRule productElimination rename thin setElimination sqequalHypSubstitution cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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