---

Step * 1 1 of Lemma grp_inv_inv


1. g : IGroup
2. a : |g|
⊢ ((~ a) * (~ (~ a))) = ((~ a) * a) ∈ |g|
BY
{ RWH (FirstC(map (\i.GenLemmaC i `grp_inverse`) [1;2])) 0 THENA Auto }

1
1. g : IGroup
2. a : |g|
⊢ e = e ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  a  :  |g|
\mvdash{}  ((\msim{}  a)  *  (\msim{}  (\msim{}  a)))  =  ((\msim{}  a)  *  a)


By

---

Latex:
RWH  (FirstC(map  (\mbackslash{}i.GenLemmaC  i  `grp\_inverse`)  [1;2]))  0  THENA  Auto

---

Home Index