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

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

let v1 be Vector of V; :: according to BILINEAR:def 11 :: thesis: FunctionalFAF (f,v1) is additive

set F = FunctionalFAF (f,v1);

set F2 = FunctionalSAF (f,v1);

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

let v1 be Vector of V; :: according to BILINEAR:def 11 :: thesis: FunctionalFAF (f,v1) is additive

set F = FunctionalFAF (f,v1);

set F2 = FunctionalSAF (f,v1);

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

hence
FunctionalFAF (f,v1) is additive
; :: thesis: verumlet x, y be Vector of V; :: thesis: (FunctionalFAF (f,v1)) . (x + y) = ((FunctionalFAF (f,v1)) . x) + ((FunctionalFAF (f,v1)) . y)

thus (FunctionalFAF (f,v1)) . (x + y) = f . (v1,(x + y)) by BILINEAR:8

.= (f . ((x + y),v1)) *' by A1

.= ((FunctionalSAF (f,v1)) . (x + y)) *' by BILINEAR:9

.= (((FunctionalSAF (f,v1)) . x) + ((FunctionalSAF (f,v1)) . y)) *' by A1, VECTSP_1:def 20

.= ((f . (x,v1)) + ((FunctionalSAF (f,v1)) . y)) *' by BILINEAR:9

.= ((f . (x,v1)) + (f . (y,v1))) *' by BILINEAR:9

.= ((f . (x,v1)) *') + ((f . (y,v1)) *') by COMPLFLD:51

.= (f . (v1,x)) + ((f . (y,v1)) *') by A1

.= (f . (v1,x)) + (f . (v1,y)) by A1

.= ((FunctionalFAF (f,v1)) . x) + (f . (v1,y)) by BILINEAR:8

.= ((FunctionalFAF (f,v1)) . x) + ((FunctionalFAF (f,v1)) . y) by BILINEAR:8 ; :: thesis: verum

end;thus (FunctionalFAF (f,v1)) . (x + y) = f . (v1,(x + y)) by BILINEAR:8

.= (f . ((x + y),v1)) *' by A1

.= ((FunctionalSAF (f,v1)) . (x + y)) *' by BILINEAR:9

.= (((FunctionalSAF (f,v1)) . x) + ((FunctionalSAF (f,v1)) . y)) *' by A1, VECTSP_1:def 20

.= ((f . (x,v1)) + ((FunctionalSAF (f,v1)) . y)) *' by BILINEAR:9

.= ((f . (x,v1)) + (f . (y,v1))) *' by BILINEAR:9

.= ((f . (x,v1)) *') + ((f . (y,v1)) *') by COMPLFLD:51

.= (f . (v1,x)) + ((f . (y,v1)) *') by A1

.= (f . (v1,x)) + (f . (v1,y)) by A1

.= ((FunctionalFAF (f,v1)) . x) + (f . (v1,y)) by BILINEAR:8

.= ((FunctionalFAF (f,v1)) . x) + ((FunctionalFAF (f,v1)) . y) by BILINEAR:8 ; :: thesis: verum