---

Step * of Lemma algebra_bilinear

∀[A:Rng]. ∀[m:algebra{i:l}(A)]. ∀[a,x,y:m.car].
  (((a m.times (x m.plus y)) = ((a m.times x) m.plus (a m.times y)) ∈ m.car)
  ∧ (((x m.plus y) m.times a) = ((x m.times a) m.plus (y m.times a)) ∈ m.car))
BY
{ ((ProvePropertyLemma `bilinear` 2) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Rng].  \mforall{}[m:algebra\{i:l\}(A)].  \mforall{}[a,x,y:m.car].
    (((a  m.times  (x  m.plus  y))  =  ((a  m.times  x)  m.plus  (a  m.times  y)))
    \mwedge{}  (((x  m.plus  y)  m.times  a)  =  ((x  m.times  a)  m.plus  (y  m.times  a))))


By

---

Latex:
((ProvePropertyLemma  `bilinear`  2)  THEN  Auto)

---

Home Index