Step
*
of Lemma
vs-map-subtract
∀[K:Rng]. ∀[A,B:VectorSpace(K)]. ∀[f:A ⟶ B]. ∀[x,y:Point(A)].  ((f (x - y)) = (f x - f y) ∈ Point(B))
BY
{ (Auto THEN DVar `f' THEN ExRepD THEN RepUR ``vs-subtract`` 0 THEN RWW "5 6" 0 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