let V be RealLinearSpace; :: thesis: for p, q, r, u, u1, u2 being Element of V holds ((p + q) + r) + ((u + u2) + u1) = ((p + u) + (q + u2)) + (r + u1)
let p, q, r, u, u1, u2 be Element of V; :: thesis: ((p + q) + r) + ((u + u2) + u1) = ((p + u) + (q + u2)) + (r + u1)
thus ((p + u) + (q + u2)) + (r + u1) = (u + (p + (q + u2))) + (r + u1) by RLVECT_1:def 3
.= (u + ((p + q) + u2)) + (r + u1) by RLVECT_1:def 3
.= ((u + u2) + (p + q)) + (r + u1) by RLVECT_1:def 3
.= (u + u2) + ((p + q) + (r + u1)) by RLVECT_1:def 3
.= (u + u2) + (((p + q) + r) + u1) by RLVECT_1:def 3
.= ((p + q) + r) + ((u + u2) + u1) by RLVECT_1:def 3 ; :: thesis: verum