Step
*
of Lemma
monoid_hom_id
∀[g,h:GrpSig]. ∀[f:MonHom(g,h)]. ((f e) = e ∈ |h|)
BY
{ ((UnivCD) THENA Auto) }
1
1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
⊢ (f e) = e ∈ |h|
Latex:
Latex:
\mforall{}[g,h:GrpSig]. \mforall{}[f:MonHom(g,h)]. ((f e) = e)
By
Latex:
((UnivCD) THENA Auto)
Home
Index