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:39
.= (x1 + x2) + ((- y1) + (- y2)) by RVSUM_1:15
.= (x1 - y1) + (x2 - y2) by Th16 ; :: thesis: verum