---

Step * of Lemma omral_times_comm

∀g:OCMon. ∀a:CDRng.  Comm(|omral(g;a)|;λps,qs. (ps ** qs))
BY
{ Force `5` (Eval ``comm`` 0) 
THEN RenameBVars [`x',`ps';`y',`qs'] 0 
THEN ((RepD) THENA Auto) 
 }

1
1. g : OCMon
2. a : CDRng
3. ps : |omral(g;a)|
4. qs : |omral(g;a)|
⊢ (ps ** qs) = (qs ** ps) ∈ |omral(g;a)|

---

Latex:

---

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


By

---

Latex:
Force  `5`  (Eval  ``comm``  0) 
THEN  RenameBVars  [`x',`ps';`y',`qs']  0 
THEN  ((RepD)  THENA  Auto) 

---

Home Index