---

Step * 1 of Lemma monoid_hom_properties


∀[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|))
BY
{ ProvePropertiesLemma }

---

Latex:

---

Latex:

\mforall{}[g,h:GrpSig].  \mforall{}[f:\{f:|g|  {}\mrightarrow{}  |h|| 
                                        (\mforall{}[a1,a2:|g|].    ((f  (a1  *  a2))  =  ((f  a1)  *  (f  a2))))  \mwedge{}  ((f  e)  =  e)\}  ].
    ((\mforall{}[a1,a2:|g|].    ((f  (a1  *  a2))  =  ((f  a1)  *  (f  a2))))  \mwedge{}  ((f  e)  =  e))


By

---

Latex:
ProvePropertiesLemma

---

Home Index