---

Step * 1 of Lemma omral_times_ident_r


1. g : OCMon
2. r : CDRng
3. ps : |omral(g;r)|
4. Comm(|omral(g;r)|;λps,qs. (ps ** qs))
⊢ (ps ** 11) = ps ∈ |omral(g;r)|
BY
{ ((Force `5` (Eval ``comm`` (-1)) 
THENM RWH (HypC (-1)) 0  
THENM BLemma `omral_times_ident_l`) THENA Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  ps  :  |omral(g;r)|
4.  Comm(|omral(g;r)|;\mlambda{}ps,qs.  (ps  **  qs))
\mvdash{}  (ps  **  11)  =  ps


By

---

Latex:
((Force  `5`  (Eval  ``comm``  (-1)) 
THENM  RWH  (HypC  (-1))  0   
THENM  BLemma  `omral\_times\_ident\_l`)  THENA  Auto)

---

Home Index