let K be non empty addLoopStr ; for V, W being non empty ModuleStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
let V, W be non empty ModuleStr over K; for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
let f, g be Form of V,W; for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
let w be Vector of W; FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
now for v being Vector of V holds (FunctionalSAF ((f - g),w)) . v = ((FunctionalSAF (f,w)) - (FunctionalSAF (g,w))) . vlet v be
Vector of
V;
(FunctionalSAF ((f - g),w)) . v = ((FunctionalSAF (f,w)) - (FunctionalSAF (g,w))) . vthus (FunctionalSAF ((f - g),w)) . v =
(f - g) . (
v,
w)
by Th9
.=
(f . (v,w)) - (g . (v,w))
by Def7
.=
((FunctionalSAF (f,w)) . v) - (g . (v,w))
by Th9
.=
((FunctionalSAF (f,w)) . v) - ((FunctionalSAF (g,w)) . v)
by Th9
.=
((FunctionalSAF (f,w)) . v) + (- ((FunctionalSAF (g,w)) . v))
by RLVECT_1:def 11
.=
((FunctionalSAF (f,w)) . v) + ((- (FunctionalSAF (g,w))) . v)
by HAHNBAN1:def 4
.=
((FunctionalSAF (f,w)) - (FunctionalSAF (g,w))) . v
by HAHNBAN1:def 3
;
verum end;
hence
FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
by FUNCT_2:63; verum