---

Step * of Lemma abmonoid_comm

∀[g:IAbMonoid]. ∀[a,b:|g|].  ((a * b) = (b * a) ∈ |g|)
BY
{ Fold `comm` 0 THEN UnivCD THENA Auto }

1
1. g : IAbMonoid
⊢ Comm(|g|;*)

---

Latex:

---

Latex:
\mforall{}[g:IAbMonoid].  \mforall{}[a,b:|g|].    ((a  *  b)  =  (b  *  a))


By

---

Latex:
Fold  `comm`  0  THEN  UnivCD  THENA  Auto

---

Home Index