let v, w be Vector of V; :: according to GRCAT_1:def 13 :: thesis: (f *' ) . (v + w) = ((f *' ) . v) + ((f *' ) . w)
thus (f *' ) . (v + w) = (f . (v + w)) *' by Def2
.= ((f . v) + (f . w)) *' by GRCAT_1:def 13
.= ((f . v) *' ) + ((f . w) *' ) by COMPLFLD:87
.= ((f *' ) . v) + ((f . w) *' ) by Def2
.= ((f *' ) . v) + ((f *' ) . w) by Def2 ; :: thesis: verum