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);

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)

hence
FunctionalFAF (f,v1) is cmplxhomogeneous
; :: thesis: verumfor 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;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