let w be Vector of W; :: according to BILINEAR:def 12 :: thesis: FunctionalSAF ((f *'),w) is additive
let v, t be Vector of V; :: according to VECTSP_1:def 19 :: 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:9
.= (f . ((v + t),w)) *' by Def8
.= ((f . (v,w)) + (f . (t,w))) *' by BILINEAR:26
.= ((f . (v,w)) *') + ((f . (t,w)) *') by COMPLFLD:51
.= ((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:9
.= ((FunctionalSAF ((f *'),w)) . v) + ((FunctionalSAF ((f *'),w)) . t) by BILINEAR:9 ; :: thesis: verum