---

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