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