---

Step * of Lemma omral_bilinear_a

∀g:OCMon. ∀a:CDRng.
  ∀[ps,qs,rs:|omral(g;a)|].
    (((ps ** (qs ++ rs)) = ((ps ** qs) ++ (ps ** rs)) ∈ |omral(g;a)|)
    ∧ (((qs ++ rs) ** ps) = ((qs ** ps) ++ (rs ** ps)) ∈ |omral(g;a)|))
BY
{ AssertLemma `omral_bilinear` [] 
THEN Force `5` (Eval ``bilinear`` 1) 
THEN Trivial }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}a:CDRng.
    \mforall{}[ps,qs,rs:|omral(g;a)|].
        (((ps  **  (qs  ++  rs))  =  ((ps  **  qs)  ++  (ps  **  rs)))
        \mwedge{}  (((qs  ++  rs)  **  ps)  =  ((qs  **  ps)  ++  (rs  **  ps))))


By

---

Latex:
AssertLemma  `omral\_bilinear`  [] 
THEN  Force  `5`  (Eval  ``bilinear``  1) 
THEN  Trivial

---

Home Index