---

Step * of Lemma rv-sep-shift2

∀rv:InnerProductSpace. ∀a,p,q:Point.  (p # q ⇒ p + a # q + a)
BY
{ Auto }

1
1. rv : InnerProductSpace
2. a : Point
3. p : Point
4. q : Point
5. p # q
⊢ p + a # q + a

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,p,q:Point.    (p  \#  q  {}\mRightarrow{}  p  +  a  \#  q  +  a)


By

---

Latex:
Auto

---

Home Index