let x, y be Vector of V; :: according to VECTSP_1:def 19 :: thesis: (f + g) . (x + y) = ((f + g) . x) + ((f + g) . y)
thus (f + g) . (x + y) = (f . (x + y)) + (g . (x + y)) by Def3
.= ((f . x) + (f . y)) + (g . (x + y)) by VECTSP_1:def 20
.= ((f . x) + (f . y)) + ((g . x) + (g . y)) by VECTSP_1:def 20
.= (f . x) + ((f . y) + ((g . x) + (g . y))) by RLVECT_1:def 3
.= (f . x) + ((g . x) + ((f . y) + (g . y))) by RLVECT_1:def 3
.= ((f . x) + (g . x)) + ((f . y) + (g . y)) by RLVECT_1:def 3
.= ((f + g) . x) + ((f . y) + (g . y)) by Def3
.= ((f + g) . x) + ((f + g) . y) by Def3 ; :: thesis: verum