let V be RealLinearSpace; 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; ((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
; verum