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:16
.= a * ((FunctionalFAF f,w) . (b * v)) by HAHNBAN1:def 9
.= a * ((b *' ) * ((FunctionalFAF f,w) . v)) by Def1
.= (b *' ) * (a * ((FunctionalFAF f,w) . v))
.= (b *' ) * ((a * (FunctionalFAF f,w)) . v) by HAHNBAN1:def 9
.= (b *' ) * ((FunctionalFAF (a * f),w) . v) by BILINEAR:16 ; :: thesis: verum