---

Step * of Lemma perm_mon_ident

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

---

Latex:

---

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


By

---

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

---

Home Index