let v be Vector of V; :: according to BILINEAR:def 11 :: thesis: FunctionalFAF ((f *'),v) is additive
let w, t be Vector of W; :: according to VECTSP_1:def 19 :: thesis: (FunctionalFAF ((f *'),v)) . (w + t) = ((FunctionalFAF ((f *'),v)) . w) + ((FunctionalFAF ((f *'),v)) . t)
set fg = FunctionalFAF ((f *'),v);
thus (FunctionalFAF ((f *'),v)) . (w + t) = (f *') . (v,(w + t)) by BILINEAR:8
.= (f . (v,(w + t))) *' by Def8
.= ((f . (v,w)) + (f . (v,t))) *' by BILINEAR:27
.= ((f . (v,w)) *') + ((f . (v,t)) *') by COMPLFLD:51
.= ((f *') . (v,w)) + ((f . (v,t)) *') by Def8
.= ((f *') . (v,w)) + ((f *') . (v,t)) by Def8
.= ((FunctionalFAF ((f *'),v)) . w) + ((f *') . (v,t)) by BILINEAR:8
.= ((FunctionalFAF ((f *'),v)) . w) + ((FunctionalFAF ((f *'),v)) . t) by BILINEAR:8 ; :: thesis: verum