let w be Vector of V; :: according to ZMODLAT1:def 27 :: thesis: FrFunctionalFAF ((a * f),w) is additive
set Ffg = FrFunctionalFAF ((a * f),w);
set Ff = FrFunctionalFAF (f,w);
let v, y be Vector of W; :: according to VECTSP_1:def 19 :: thesis: (FrFunctionalFAF ((a * f),w)) . (v + y) = ((FrFunctionalFAF ((a * f),w)) . v) + ((FrFunctionalFAF ((a * f),w)) . y)
A1: FrFunctionalFAF (f,w) is additive ;
thus (FrFunctionalFAF ((a * f),w)) . (v + y) = (a * (FrFunctionalFAF (f,w))) . (v + y) by HTh15
.= a * ((FrFunctionalFAF (f,w)) . (v + y)) by HDef6
.= a * (((FrFunctionalFAF (f,w)) . v) + ((FrFunctionalFAF (f,w)) . y)) by A1
.= (a * ((FrFunctionalFAF (f,w)) . v)) + (a * ((FrFunctionalFAF (f,w)) . y))
.= ((a * (FrFunctionalFAF (f,w))) . v) + (a * ((FrFunctionalFAF (f,w)) . y)) by HDef6
.= ((a * (FrFunctionalFAF (f,w))) . v) + ((a * (FrFunctionalFAF (f,w))) . y) by HDef6
.= ((FrFunctionalFAF ((a * f),w)) . v) + ((a * (FrFunctionalFAF (f,w))) . y) by HTh15
.= ((FrFunctionalFAF ((a * f),w)) . v) + ((FrFunctionalFAF ((a * f),w)) . y) by HTh15 ; :: thesis: verum