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