Step * of Lemma vs-map-subtract

[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[x,y:Point(A)].  ((f (x y)) (f y) ∈ Point(B))
BY
(Auto THEN DVar `f' THEN ExRepD THEN RepUR ``vs-subtract`` THEN RWW "5 6" THEN Auto) }


Latex:


Latex:
\mforall{}[K:Rng].  \mforall{}[A,B:VectorSpace(K)].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[x,y:Point(A)].    ((f  (x  -  y))  =  (f  x  -  f  y))


By


Latex:
(Auto  THEN  DVar  `f'  THEN  ExRepD  THEN  RepUR  ``vs-subtract``  0  THEN  RWW  "5  6"  0  THEN  Auto)




Home Index