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 HDef3
.= ((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) + (g . x)) + ((f . y) + (g . y))
.= ((f + g) . x) + ((f . y) + (g . y)) by HDef3
.= ((f + g) . x) + ((f + g) . y) by HDef3 ; :: thesis: verum