let f be Form of V,V; :: thesis: ( f is hermitan & f is homogeneousSAF implies f is cmplxhomogeneousFAF )
assume A1: ( f is hermitan & f is homogeneousSAF ) ; :: thesis: f is cmplxhomogeneousFAF
let v1 be Vector of V; :: according to HERMITAN:def 4 :: thesis: FunctionalFAF f,v1 is cmplxhomogeneous
set F = FunctionalFAF f,v1;
set F2 = FunctionalSAF f,v1;

now

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

end;

hence FunctionalFAF f,v1 is cmplxhomogeneous by Def1; :: thesis: verum