---

Step * of Lemma monoid_hom_p_wf

∀[a,b:GrpSig]. ∀[f:|a| ⟶ |b|].  (IsMonHom{a,b}(f) ∈ ℙ)
BY
{ Unfold `monoid_hom_p` 0 THEN Auto⋅ }

---

Latex:

---

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


By

---

Latex:
Unfold  `monoid\_hom\_p`  0  THEN  Auto\mcdot{}

---

Home Index