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 13 :: thesis: FunctionalSAF f,w is additive
set F = FunctionalSAF f,w;
set F1 = FunctionalFAF f,w;

now

let 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:10
.= (f . w,(x + y)) *' by A1, Def5
.= ((FunctionalFAF f,w) . (x + y)) *' by BILINEAR:9
.= (((FunctionalFAF f,w) . x) + ((FunctionalFAF f,w) . y)) *' by A1, GRCAT_1:def 13
.= ((f . w,x) + ((FunctionalFAF f,w) . y)) *' by BILINEAR:9
.= ((f . w,x) + (f . w,y)) *' by BILINEAR:9
.= ((f . w,x) *' ) + ((f . w,y) *' ) by COMPLFLD:87
.= (f . x,w) + ((f . w,y) *' ) by A1, Def5
.= (f . x,w) + (f . y,w) by A1, Def5
.= ((FunctionalSAF f,w) . x) + (f . y,w) by BILINEAR:10
.= ((FunctionalSAF f,w) . x) + ((FunctionalSAF f,w) . y) by BILINEAR:10 ; :: thesis: verum

end;

hence FunctionalSAF f,w is additive by GRCAT_1:def 13; :: thesis: verum