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