---

Step * 7 of Lemma omral_alg_wf2


1. g : OCMon
2. r : CDRng
3. IsMonoid(omral_alg(g;r).car;omral_alg(g;r).times;omral_alg(g;r).one)
⊢ BiLinear(omral_alg(g;r).car;omral_alg(g;r).plus;omral_alg(g;r).times)
BY
{ RWH AbRedexC 0 
THENM ((BLemma `omral_bilinear`) THENA Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
RWH  AbRedexC  0 
THENM  ((BLemma  `omral\_bilinear`)  THENA  Auto)

---

Home Index