let w be Vector of W; :: according to BILINEAR:def 13 :: thesis: FunctionalSAF (- f),w is additive
set Ffg = FunctionalSAF (- f),w;
set Ff = FunctionalSAF f,w;
let v, y be Vector of V; :: according to GRCAT_1:def 13 :: thesis: (FunctionalSAF (- f),w) . (v + y) = ((FunctionalSAF (- f),w) . v) + ((FunctionalSAF (- f),w) . y)
A1: FunctionalSAF f,w is additive by Def13;
thus (FunctionalSAF (- f),w) . (v + y) = (- (FunctionalSAF f,w)) . (v + y) by Th17
.= - ((FunctionalSAF f,w) . (v + y)) by HAHNBAN1:def 7
.= - (((FunctionalSAF f,w) . v) + ((FunctionalSAF f,w) . y)) by A1, GRCAT_1:def 13
.= (- ((FunctionalSAF f,w) . v)) - ((FunctionalSAF f,w) . y) by RLVECT_1:44
.= ((- (FunctionalSAF f,w)) . v) - ((FunctionalSAF f,w) . y) by HAHNBAN1:def 7
.= ((- (FunctionalSAF f,w)) . v) + (- ((FunctionalSAF f,w) . y)) by RLVECT_1:def 14
.= ((- (FunctionalSAF f,w)) . v) + ((- (FunctionalSAF f,w)) . y) by HAHNBAN1:def 7
.= ((FunctionalSAF (- f),w) . v) + ((- (FunctionalSAF f,w)) . y) by Th17
.= ((FunctionalSAF (- f),w) . v) + ((FunctionalSAF (- f),w) . y) by Th17 ; :: thesis: verum