---

Step * 6 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
⊢ IsMonoid(omral_alg(g;r).car;omral_alg(g;r).times;omral_alg(g;r).one)
BY
{ RWH AbRedexC 0 
THENM D 0 }

1
1. g : OCMon
2. r : CDRng
⊢ Assoc(|omral(g;r)|;λx,y. (x ** y))

2
1. g : OCMon
2. r : CDRng
⊢ Ident(|omral(g;r)|;λx,y. (x ** y);11)

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  r  :  CDRng
\mvdash{}  IsMonoid(omral\_alg(g;r).car;omral\_alg(g;r).times;omral\_alg(g;r).one)


By

---

Latex:
RWH  AbRedexC  0 
THENM  D  0

---

Home Index