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