let x, y be Vector of V; :: according to VECTSP_1:def 19 :: thesis: (v * f) . (x + y) = ((v * f) . x) + ((v * f) . y)
thus (v * f) . (x + y) = v * (f . (x + y)) by Def6
.= v * ((f . x) + (f . y)) by VECTSP_1:def 20
.= (v * (f . x)) + (v * (f . y)) by VECTSP_1:def 2
.= ((v * f) . x) + (v * (f . y)) by Def6
.= ((v * f) . x) + ((v * f) . y) by Def6 ; :: thesis: verum