let w be Vector of V; :: according to HERMITAN:def 4 :: thesis: FunctionalFAF ((f + g),w) is cmplxhomogeneous
set Ffg = FunctionalFAF ((f + g),w);
set Ff = FunctionalFAF (f,w);
set Fg = FunctionalFAF (g,w);
let v be Vector of W; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (FunctionalFAF ((f + g),w)) . (a * v) = (a *') * ((FunctionalFAF ((f + g),w)) . v)
let a be Scalar of ; :: thesis: (FunctionalFAF ((f + g),w)) . (a * v) = (a *') * ((FunctionalFAF ((f + g),w)) . v)
thus (FunctionalFAF ((f + g),w)) . (a * v) = ((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . (a * v) by BILINEAR:13
.= ((FunctionalFAF (f,w)) . (a * v)) + ((FunctionalFAF (g,w)) . (a * v)) by HAHNBAN1:def 3
.= ((a *') * ((FunctionalFAF (f,w)) . v)) + ((FunctionalFAF (g,w)) . (a * v)) by Def1
.= ((a *') * ((FunctionalFAF (f,w)) . v)) + ((a *') * ((FunctionalFAF (g,w)) . v)) by Def1
.= (a *') * (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (g,w)) . v))
.= (a *') * (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) by HAHNBAN1:def 3
.= (a *') * ((FunctionalFAF ((f + g),w)) . v) by BILINEAR:13 ; :: thesis: verum