---

Step * of Lemma monoid_hom_properties

∀[g,h:GrpSig]. ∀[f:MonHom(g,h)].  IsMonHom{g,h}(f)
BY
{ RepUnfolds ``monoid_hom monoid_hom_p fun_thru_2op`` 0 }

1
∀[g,h:GrpSig]. ∀[f:{f:|g| ⟶ |h|| (∀[a1,a2:|g|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)) ∧ ((f e) = e ∈ |h|)} ].
  ((∀[a1,a2:|g|].  ((f (a1 * a2)) = ((f a1) * (f a2)) ∈ |h|)) ∧ ((f e) = e ∈ |h|))

---

Latex:

---

Latex:
\mforall{}[g,h:GrpSig].  \mforall{}[f:MonHom(g,h)].    IsMonHom\{g,h\}(f)


By

---

Latex:
RepUnfolds  ``monoid\_hom  monoid\_hom\_p  fun\_thru\_2op``  0

---

Home Index