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