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;
let v, y be Vector of W; :: according to GRCAT_1:def 13 :: thesis: (FunctionalFAF (- f),w) . (v + y) = ((FunctionalFAF (- f),w) . v) + ((FunctionalFAF (- f),w) . y)
A1: FunctionalFAF f,w is additive by Def12;
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, GRCAT_1:def 13
.= (- ((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 14
.= ((- (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