∀[g,h:GrpSig]. ∀[f:MonHom(g,h)].  ((f e) = e ∈ |h|)
{ ((UnivCD) THENA Auto) }
1. g : GrpSig
2. h : GrpSig
3. f : MonHom(g,h)
⊢ (f e) = e ∈ |h|