---

Step * of Lemma perm_grp_inverse

∀[T:Type]. ∀[a:Perm(T)].  ((a O inv_perm(a) = id_perm() ∈ Perm(T)) ∧ (inv_perm(a) O a = id_perm() ∈ Perm(T)))
BY
{ (ProveSpecializedLemma `grp_inverse` 1 [parm{i}; perm_igrp(T)] (AbReduceC)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a:Perm(T)].    ((a  O  inv\_perm(a)  =  id\_perm())  \mwedge{}  (inv\_perm(a)  O  a  =  id\_perm()))


By

---

Latex:
(ProveSpecializedLemma  `grp\_inverse`  1  [parm\{i\};  perm\_igrp(T)]  (AbReduceC))

---

Home Index