let f be Form of V,V; ( f is hermitan & f is cmplxhomogeneousFAF implies f is homogeneousSAF )
assume A1:
( f is hermitan & f is cmplxhomogeneousFAF )
; f is homogeneousSAF
let w be Vector of V; BILINEAR:def 14 FunctionalSAF (f,w) is homogeneous
set F = FunctionalSAF (f,w);
set F2 = FunctionalFAF (f,w);
A2:
FunctionalFAF (f,w) is cmplxhomogeneous
by A1;
now 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;
for r being Scalar of holds (FunctionalSAF (f,w)) . (r * x) = r * ((FunctionalSAF (f,w)) . x)let r be
Scalar of ;
(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
;
verum end;
hence
FunctionalSAF (f,w) is homogeneous
; verum