let X be RealNormSpace; :: 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