let n be Nat; :: thesis: for a, b, c being Element of REAL n holds ((a - b) + c) + b = a + c
let a, b, c be Element of REAL n; :: thesis: ((a - b) + c) + b = a + c
reconsider a2 = a, b2 = b, c2 = c as Element of n -tuples_on REAL ;
((a2 - b2) + c2) + b2 = ((a2 + (- b2)) + b2) + c2 by RFUNCT_1:8
.= (a2 + (b2 + (- b2))) + c2 by RFUNCT_1:8
.= (a2 + (n |-> (In (0,REAL)))) + c2 by RVSUM_1:22
.= a2 + c2 by RVSUM_1:16 ;
hence ((a - b) + c) + b = a + c ; :: thesis: verum