let f be Form of V,V; ( f is hermitan & f is additiveFAF implies f is additiveSAF )
assume A1:
( f is hermitan & f is additiveFAF )
; f is additiveSAF
let w be Vector of V; BILINEAR:def 12 FunctionalSAF (f,w) is additive
set F = FunctionalSAF (f,w);
set F1 = FunctionalFAF (f,w);
now for x, y being Vector of V holds (FunctionalSAF (f,w)) . (x + y) = ((FunctionalSAF (f,w)) . x) + ((FunctionalSAF (f,w)) . y)let x,
y be
Vector of
V;
(FunctionalSAF (f,w)) . (x + y) = ((FunctionalSAF (f,w)) . x) + ((FunctionalSAF (f,w)) . y)thus (FunctionalSAF (f,w)) . (x + y) =
f . (
(x + y),
w)
by BILINEAR:9
.=
(f . (w,(x + y))) *'
by A1
.=
((FunctionalFAF (f,w)) . (x + y)) *'
by BILINEAR:8
.=
(((FunctionalFAF (f,w)) . x) + ((FunctionalFAF (f,w)) . y)) *'
by A1, VECTSP_1:def 20
.=
((f . (w,x)) + ((FunctionalFAF (f,w)) . y)) *'
by BILINEAR:8
.=
((f . (w,x)) + (f . (w,y))) *'
by BILINEAR:8
.=
((f . (w,x)) *') + ((f . (w,y)) *')
by COMPLFLD:51
.=
(f . (x,w)) + ((f . (w,y)) *')
by A1
.=
(f . (x,w)) + (f . (y,w))
by A1
.=
((FunctionalSAF (f,w)) . x) + (f . (y,w))
by BILINEAR:9
.=
((FunctionalSAF (f,w)) . x) + ((FunctionalSAF (f,w)) . y)
by BILINEAR:9
;
verum end;
hence
FunctionalSAF (f,w) is additive
; verum