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