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 14 :: thesis: FunctionalSAF (f,w) is homogeneous
set F = FunctionalSAF (f,w);
set F2 = FunctionalFAF (f,w);
A2: FunctionalFAF (f,w) is cmplxhomogeneous by A1;

now :: thesis: for x being Vector of V
for r being Scalar of holds (FunctionalSAF (f,w)) . (r * x) = r * ((FunctionalSAF (f,w)) . x)

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:9
.= (f . (w,(r * x))) *' by A1
.= ((FunctionalFAF (f,w)) . (r * x)) *' by BILINEAR:8
.= ((r *') * ((FunctionalFAF (f,w)) . x)) *' by A2
.= ((r *') *') * (((FunctionalFAF (f,w)) . x) *') by COMPLFLD:54
.= r * ((f . (w,x)) *') by BILINEAR:8
.= r * (f . (x,w)) by A1
.= r * ((FunctionalSAF (f,w)) . x) by BILINEAR:9 ; :: thesis: verum

end;

hence FunctionalSAF (f,w) is homogeneous ; :: thesis: verum