let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)
let x1, x2, x3 be Element of REAL n; :: thesis: - ((x1 + x2) + x3) = ((- x1) + (- x2)) + (- x3)
thus - ((x1 + x2) + x3) = (0* n) - ((x1 + x2) + x3) by RVSUM_1:33
.= ((0* n) - (x1 + x2)) - x3 by RVSUM_1:39
.= (((0* n) - x1) - x2) - x3 by RVSUM_1:39
.= ((- x1) + (- x2)) + (- x3) by RVSUM_1:33 ; :: thesis: verum