---

Step * of Lemma rv-mul-add

∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point].  a*x + b*x ≡ a + b*x
BY
{ (Auto THEN (BLemma `ss-eq_inversion` THENA Auto)) }

1
1. rv : RealVectorSpace
2. a : ℝ
3. b : ℝ
4. x : Point
⊢ a + b*x ≡ a*x + b*x

---

Latex:

---

Latex:
\mforall{}[rv:RealVectorSpace].  \mforall{}[a,b:\mBbbR{}].  \mforall{}[x:Point].    a*x  +  b*x  \mequiv{}  a  +  b*x


By

---

Latex:
(Auto  THEN  (BLemma  `ss-eq\_inversion`  THENA  Auto))

---

Home Index