let f be Form of V,V; :: thesis: ( f is hermitan & f is cmplxhomogeneousFAF implies f is homogeneousSAF )
assume A1: ( f is hermitan & f is cmplxhomogeneousFAF ) ; :: thesis: f is homogeneousSAF
let w be Vector of V; :: according to BILINEAR:def 15 :: thesis: FunctionalSAF f,w is homogeneous
set F = FunctionalSAF f,w;
set F2 = FunctionalFAF f,w;
A2: FunctionalFAF f,w is cmplxhomogeneous by A1, Def4;

now

let x be Vector of V; :: thesis: for r being Scalar of holds (FunctionalSAF f,w) . (r * x) = r * ((FunctionalSAF f,w) . x)
let r be Scalar of ; :: thesis: (FunctionalSAF f,w) . (r * x) = r * ((FunctionalSAF f,w) . x)
thus (FunctionalSAF f,w) . (r * x) = f . (r * x),w by BILINEAR:10
.= (f . w,(r * x)) *' by A1, Def5
.= ((FunctionalFAF f,w) . (r * x)) *' by BILINEAR:9
.= ((r *' ) * ((FunctionalFAF f,w) . x)) *' by A2, Def1
.= ((r *' ) *' ) * (((FunctionalFAF f,w) . x) *' ) by COMPLFLD:90
.= r * ((f . w,x) *' ) by BILINEAR:9
.= r * (f . x,w) by A1, Def5
.= r * ((FunctionalSAF f,w) . x) by BILINEAR:10 ; :: thesis: verum

end;

hence FunctionalSAF f,w is homogeneous by HAHNBAN1:def 12; :: thesis: verum