---

Step * of Lemma grp_inverse

∀[g:IGroup]. ∀[a:|g|].  (((a * (~ a)) = e ∈ |g|) ∧ (((~ a) * a) = e ∈ |g|))
BY
{ Fold `inverse` 0 THEN D 0 
THENM D 1 THEN Auto }

---

Latex:

---

Latex:
\mforall{}[g:IGroup].  \mforall{}[a:|g|].    (((a  *  (\msim{}  a))  =  e)  \mwedge{}  (((\msim{}  a)  *  a)  =  e))


By

---

Latex:
Fold  `inverse`  0  THEN  D  0 
THENM  D  1  THEN  Auto

---

Home Index