Step
*
of Lemma
mon_ident
∀[g:IMonoid]. ∀[a:|g|].  (((a * e) = a ∈ |g|) ∧ ((e * a) = a ∈ |g|))
BY
{ Fold `ident` 0  
THEN UnivCD THENA Auto }
1
1. g : IMonoid
⊢ Ident(|g|;*;e)
Latex:
Latex:
\mforall{}[g:IMonoid].  \mforall{}[a:|g|].    (((a  *  e)  =  a)  \mwedge{}  ((e  *  a)  =  a))
By
Latex:
Fold  `ident`  0   
THEN  UnivCD  THENA  Auto
Home
Index