let w be Vector of W; :: according to BILINEAR:def 13 :: thesis: FunctionalSAF (f *' ),w is additive
let v, t be Vector of V; :: according to HAHNBAN1:def 11 :: thesis: (FunctionalSAF (f *' ),w) . (v + t) = ((FunctionalSAF (f *' ),w) . v) + ((FunctionalSAF (f *' ),w) . t)
set fg = FunctionalSAF (f *' ),w;
thus (FunctionalSAF (f *' ),w) . (v + t) = (f *' ) . (v + t),w by BILINEAR:10
.= (f . (v + t),w) *' by Def8
.= ((f . v,w) + (f . t,w)) *' by BILINEAR:27
.= ((f . v,w) *' ) + ((f . t,w) *' ) by COMPLFLD:87
.= ((f *' ) . v,w) + ((f . t,w) *' ) by Def8
.= ((f *' ) . v,w) + ((f *' ) . t,w) by Def8
.= ((FunctionalSAF (f *' ),w) . v) + ((f *' ) . t,w) by BILINEAR:10
.= ((FunctionalSAF (f *' ),w) . v) + ((FunctionalSAF (f *' ),w) . t) by BILINEAR:10 ; :: thesis: verum