let w be Vector of V; :: according to BILINEAR:def 12 :: thesis: FunctionalFAF (a * f),w is additive
set Ffg = FunctionalFAF (a * f),w;
set Ff = FunctionalFAF f,w;
let v, y be Vector of W; :: according to HAHNBAN1:def 11 :: thesis: (FunctionalFAF (a * f),w) . (v + y) = ((FunctionalFAF (a * f),w) . v) + ((FunctionalFAF (a * f),w) . y)
A1: FunctionalFAF f,w is additive by Def12;
thus (FunctionalFAF (a * f),w) . (v + y) = (a * (FunctionalFAF f,w)) . (v + y) by Th16
.= a * ((FunctionalFAF f,w) . (v + y)) by HAHNBAN1:def 9
.= a * (((FunctionalFAF f,w) . v) + ((FunctionalFAF f,w) . y)) by A1, HAHNBAN1:def 11
.= (a * ((FunctionalFAF f,w) . v)) + (a * ((FunctionalFAF f,w) . y)) by VECTSP_1:def 11
.= ((a * (FunctionalFAF f,w)) . v) + (a * ((FunctionalFAF f,w) . y)) by HAHNBAN1:def 9
.= ((a * (FunctionalFAF f,w)) . v) + ((a * (FunctionalFAF f,w)) . y) by HAHNBAN1:def 9
.= ((FunctionalFAF (a * f),w) . v) + ((a * (FunctionalFAF f,w)) . y) by Th16
.= ((FunctionalFAF (a * f),w) . v) + ((FunctionalFAF (a * f),w) . y) by Th16 ; :: thesis: verum