---

Step * of Lemma omral_bilinear

∀g:OCMon. ∀a:CDRng.  BiLinear(|omral(g;a)|;λps,qs. (ps ++ qs);λps,qs. (ps ** qs))
BY
{ ((RepD THENM BLemma `bilinear_comm_elim` 
THENM Force `5` (Reduce 0)) THENA Auto) }

1
1. g : OCMon
2. a : CDRng
⊢ Comm(|omral(g;a)|;λps,qs. (ps ** qs))

2
1. g : OCMon
2. a : CDRng
⊢ ∀a1,x,y:|omral(g;a)|.  ((a1 ** (x ++ y)) = ((a1 ** x) ++ (a1 ** y)) ∈ |omral(g;a)|)

---

Latex:

---

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


By

---

Latex:
((RepD  THENM  BLemma  `bilinear\_comm\_elim` 
THENM  Force  `5`  (Reduce  0))  THENA  Auto)

---

Home Index