---

Step * of Lemma sq_stable__monoid_hom_p

∀[a,b:GrpSig]. ∀[f:|a| ⟶ |b|].  SqStable(IsMonHom{a,b}(f))
BY
{ ((RepUnfolds ``fun_thru_2op monoid_hom_p`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:GrpSig].  \mforall{}[f:|a|  {}\mrightarrow{}  |b|].    SqStable(IsMonHom\{a,b\}(f))


By

---

Latex:
((RepUnfolds  ``fun\_thru\_2op  monoid\_hom\_p``  0)  THEN  Auto)

---

Home Index