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 12 :: thesis: FunctionalFAF f,v1 is additive
set F = FunctionalFAF f,v1;
set F2 = FunctionalSAF f,v1;

now

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

end;

hence FunctionalFAF f,v1 is additive by GRCAT_1:def 13; :: thesis: verum