let n be Nat; :: thesis: for x1, x2, y1, y2 being Element of REAL n holds (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2)
let x1, x2, y1, y2 be Element of REAL n; :: thesis: (x1 + x2) + (y1 + y2) = (x1 + y1) + (x2 + y2)
thus (x1 + x2) + (y1 + y2) = ((x1 + x2) + y1) + y2 by RVSUM_1:15
.= ((x1 + y1) + x2) + y2 by RVSUM_1:15
.= (x1 + y1) + (x2 + y2) by RVSUM_1:15 ; :: thesis: verum