---

Step * of Lemma omral_times_comm_a

∀g:OCMon. ∀a:CDRng.  ∀[ps,qs:|omral(g;a)|].  ((ps ** qs) = (qs ** ps) ∈ |omral(g;a)|)
BY
{ AssertLemma `omral_times_comm` [] 
THEN Force `5` (Eval ``comm`` 1) 
THEN Trivial }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}a:CDRng.    \mforall{}[ps,qs:|omral(g;a)|].    ((ps  **  qs)  =  (qs  **  ps))


By

---

Latex:
AssertLemma  `omral\_times\_comm`  [] 
THEN  Force  `5`  (Eval  ``comm``  1) 
THEN  Trivial

---

Home Index