let V be RealLinearSpace; :: thesis: for u, v, w, u1, v1, w1 being Element of V holds ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
let u, v, w, u1, v1, w1 be Element of V; :: thesis: ((u + v) + w) + ((u1 + v1) + w1) = ((u + u1) + (v + v1)) + (w + w1)
thus ((u + u1) + (v + v1)) + (w + w1) = (u1 + (u + (v + v1))) + (w + w1) by RLVECT_1:def 3
.= (u1 + ((u + v) + v1)) + (w + w1) by RLVECT_1:def 3
.= ((u1 + v1) + (u + v)) + (w + w1) by RLVECT_1:def 3
.= (u1 + v1) + ((u + v) + (w + w1)) by RLVECT_1:def 3
.= (u1 + v1) + (((u + v) + w) + w1) by RLVECT_1:def 3
.= ((u + v) + w) + ((u1 + v1) + w1) by RLVECT_1:def 3 ; :: thesis: verum