---

Step * 9 1 1 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. x : omral_alg(g;r).car
4. y : omral_alg(g;r).car
⊢ (x omral_alg(g;r).times y) = (y omral_alg(g;r).times x) ∈ omral_alg(g;r).car
BY
{ ((ARepD ["basic"] 
THENM RWH AbRedexC 0 
THENM Force `2` (Reduce 0) 
THENM BLemma `omral_times_comm_a`) THENA Auto) }

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
3.  x  :  omral\_alg(g;r).car
4.  y  :  omral\_alg(g;r).car
\mvdash{}  (x  omral\_alg(g;r).times  y)  =  (y  omral\_alg(g;r).times  x)


By

---

Latex:
((ARepD  ["basic"] 
THENM  RWH  AbRedexC  0 
THENM  Force  `2`  (Reduce  0) 
THENM  BLemma  `omral\_times\_comm\_a`)  THENA  Auto)

---

Home Index