let v, w be Vector of V; :: according to GRCAT_1:def 8 :: 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 8
.= ((f . v) *') + ((f . w) *') by COMPLFLD:51
.= ((f *') . v) + ((f . w) *') by Def2
.= ((f *') . v) + ((f *') . w) by Def2 ; :: thesis: verum