let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V holds (0 * w) + (0 * y) = 0. V
let w, y be VECTOR of V; :: thesis: (0 * w) + (0 * y) = 0. V
thus (0 * w) + (0 * y) = (0. V) + (0 * y) by RLVECT_1:10
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ; :: thesis: verum