let v be Vector of V; :: according to ZMODLAT1:def 27 :: thesis: FrFunctionalFAF ((FrFormFunctional (f,g)),v) is additive
set fg = FrFormFunctional (f,g);
set F = FrFunctionalFAF ((FrFormFunctional (f,g)),v);
let y, y9 be Vector of W; :: according to VECTSP_1:def 19 :: thesis: (FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . (y + y9) = ((FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . y) + ((FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . y9)
A1: FrFunctionalFAF ((FrFormFunctional (f,g)),v) = (f . v) * g by HTh24;
hence (FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . (y + y9) = (f . v) * (g . (y + y9)) by HDef6
.= (f . v) * ((g . y) + (g . y9)) by VECTSP_1:def 20
.= ((f . v) * (g . y)) + ((f . v) * (g . y9))
.= ((f . v) * (g . y)) + ((FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . y9) by A1, HDef6
.= ((FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . y) + ((FrFunctionalFAF ((FrFormFunctional (f,g)),v)) . y9) by A1, HDef6 ;
:: thesis: verum