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:14
.= ((FunctionalFAF f,w) . (a * v)) + ((FunctionalFAF g,w) . (a * v)) by HAHNBAN1:def 6
.= ((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 6
.= (a *' ) * ((FunctionalFAF (f + g),w) . v) by BILINEAR:14 ; :: thesis: verum