let w be Vector of V; :: according to BILINEAR:def 12 :: thesis: FunctionalFAF (- f),w is additive
set Ffg = FunctionalFAF (- f),w;
set Ff = FunctionalFAF f,w;
A1: FunctionalFAF f,w is additive by Def12;
let v, y be Vector of W; :: according to HAHNBAN1:def 11 :: thesis: (FunctionalFAF (- f),w) . (v + y) = ((FunctionalFAF (- f),w) . v) + ((FunctionalFAF (- f),w) . y)
thus (FunctionalFAF (- f),w) . (v + y) = (- (FunctionalFAF f,w)) . (v + y) by Th18
.= - ((FunctionalFAF f,w) . (v + y)) by HAHNBAN1:def 7
.= - (((FunctionalFAF f,w) . v) + ((FunctionalFAF f,w) . y)) by A1, HAHNBAN1:def 11
.= (- ((FunctionalFAF f,w) . v)) - ((FunctionalFAF f,w) . y) by RLVECT_1:44
.= ((- (FunctionalFAF f,w)) . v) - ((FunctionalFAF f,w) . y) by HAHNBAN1:def 7
.= ((- (FunctionalFAF f,w)) . v) + (- ((FunctionalFAF f,w) . y)) by RLVECT_1:def 12
.= ((- (FunctionalFAF f,w)) . v) + ((- (FunctionalFAF f,w)) . y) by HAHNBAN1:def 7
.= ((FunctionalFAF (- f),w) . v) + ((- (FunctionalFAF f,w)) . y) by Th18
.= ((FunctionalFAF (- f),w) . v) + ((FunctionalFAF (- f),w) . y) by Th18 ; :: thesis: verum