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

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