let V, W be non empty ModuleStr over INT.Ring ; for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
let f, g be Form of V,W; for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
let w be Vector of V; FunctionalFAF ((f - g),w) = (FunctionalFAF (f,w)) - (FunctionalFAF (g,w))
now for v being Vector of W holds (FunctionalFAF ((f - g),w)) . v = ((FunctionalFAF (f,w)) - (FunctionalFAF (g,w))) . vlet v be
Vector of
W;
(FunctionalFAF ((f - g),w)) . v = ((FunctionalFAF (f,w)) - (FunctionalFAF (g,w))) . vthus (FunctionalFAF ((f - g),w)) . v =
(f - g) . (
w,
v)
by BLTh8
.=
(f . (w,v)) - (g . (w,v))
by BLDef7
.=
((FunctionalFAF (f,w)) . v) - (g . (w,v))
by BLTh8
.=
((FunctionalFAF (f,w)) . v) - ((FunctionalFAF (g,w)) . v)
by BLTh8
.=
((FunctionalFAF (f,w)) . v) + ((- (FunctionalFAF (g,w))) . v)
by HAHNBAN1:def 4
.=
((FunctionalFAF (f,w)) - (FunctionalFAF (g,w))) . v
by HAHNBAN1:def 3
;
verum end;
hence
FunctionalFAF ((f - g),w) = (FunctionalFAF (f,w)) - (FunctionalFAF (g,w))
by FUNCT_2:63; verum