let X be RealLinearSpace; :: thesis: for x1, x2, x3, x4 being Point of X holds (x1 + x2) + (x3 + x4) = (x1 + x3) + (x2 + x4)

let x1, x2, x3, x4 be Point of X; :: thesis: (x1 + x2) + (x3 + x4) = (x1 + x3) + (x2 + x4)

thus (x1 + x2) + (x3 + x4) = ((x1 + x2) + x3) + x4 by RLVECT_1:def 3

.= ((x1 + x3) + x2) + x4 by RLVECT_1:def 3

.= (x1 + x3) + (x2 + x4) by RLVECT_1:def 3 ; :: thesis: verum

let x1, x2, x3, x4 be Point of X; :: thesis: (x1 + x2) + (x3 + x4) = (x1 + x3) + (x2 + x4)

thus (x1 + x2) + (x3 + x4) = ((x1 + x2) + x3) + x4 by RLVECT_1:def 3

.= ((x1 + x3) + x2) + x4 by RLVECT_1:def 3

.= (x1 + x3) + (x2 + x4) by RLVECT_1:def 3 ; :: thesis: verum