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;

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)

hence
FunctionalSAF (f,w) is homogeneous
; :: thesis: verumfor 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;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