let f be Form of V,V; :: thesis: ( f is hermitan & f is additiveFAF implies f is additiveSAF )

assume A1: ( f is hermitan & f is additiveFAF ) ; :: thesis: f is additiveSAF

let w be Vector of V; :: according to BILINEAR:def 12 :: thesis: FunctionalSAF (f,w) is additive

set F = FunctionalSAF (f,w);

set F1 = FunctionalFAF (f,w);

assume A1: ( f is hermitan & f is additiveFAF ) ; :: thesis: f is additiveSAF

let w be Vector of V; :: according to BILINEAR:def 12 :: thesis: FunctionalSAF (f,w) is additive

set F = FunctionalSAF (f,w);

set F1 = FunctionalFAF (f,w);

now :: thesis: for x, y being Vector of V holds (FunctionalSAF (f,w)) . (x + y) = ((FunctionalSAF (f,w)) . x) + ((FunctionalSAF (f,w)) . y)

hence
FunctionalSAF (f,w) is additive
; :: thesis: verumlet x, y be Vector of V; :: thesis: (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 ; :: thesis: verum

end;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 ; :: thesis: verum