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