let w be Vector of V; :: according to BILINEAR:def 11 :: 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 VECTSP_1:def 19 :: thesis: (FunctionalFAF ((- f),w)) . (v + y) = ((FunctionalFAF ((- f),w)) . v) + ((FunctionalFAF ((- f),w)) . y)
A1: FunctionalFAF (f,w) is additive by Def11;
thus (FunctionalFAF ((- f),w)) . (v + y) = (- (FunctionalFAF (f,w))) . (v + y) by Th17
.= - ((FunctionalFAF (f,w)) . (v + y)) by HAHNBAN1:def 4
.= - (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) by A1
.= (- ((FunctionalFAF (f,w)) . v)) - ((FunctionalFAF (f,w)) . y) by RLVECT_1:30
.= ((- (FunctionalFAF (f,w))) . v) - ((FunctionalFAF (f,w)) . y) by HAHNBAN1:def 4
.= ((- (FunctionalFAF (f,w))) . v) + (- ((FunctionalFAF (f,w)) . y)) by RLVECT_1:def 11
.= ((- (FunctionalFAF (f,w))) . v) + ((- (FunctionalFAF (f,w))) . y) by HAHNBAN1:def 4
.= ((FunctionalFAF ((- f),w)) . v) + ((- (FunctionalFAF (f,w))) . y) by Th17
.= ((FunctionalFAF ((- f),w)) . v) + ((FunctionalFAF ((- f),w)) . y) by Th17 ; :: thesis: verum