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 :: thesis: for x being Vector of V
for r being Scalar of holds (FunctionalFAF (f,v1)) . (r * x) = (r *') * ((FunctionalFAF (f,v1)) . x)
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:8
.= (f . ((r * x),v1)) *' by A1
.= ((FunctionalSAF (f,v1)) . (r * x)) *' by BILINEAR:9
.= (r * ((FunctionalSAF (f,v1)) . x)) *' by A1, HAHNBAN1:def 8
.= (r *') * (((FunctionalSAF (f,v1)) . x) *') by COMPLFLD:54
.= (r *') * ((f . (x,v1)) *') by BILINEAR:9
.= (r *') * (f . (v1,x)) by A1
.= (r *') * ((FunctionalFAF (f,v1)) . x) by BILINEAR:8 ; :: thesis: verum
end;
hence FunctionalFAF (f,v1) is cmplxhomogeneous ; :: thesis: verum