let n be Element of NAT ; :: thesis: for f, g, h, k being Element of n -tuples_on REAL holds (f + g) - (h + k) = (f - h) + (g - k)
let f, g, h, k be Element of n -tuples_on REAL ; :: thesis: (f + g) - (h + k) = (f - h) + (g - k)
thus (f + g) - (h + k) = f + (g + (- (h + k))) by RVSUM_1:32
.= f + (g + ((- h) + (- k))) by RVSUM_1:45
.= f + ((- h) + (g + (- k))) by RVSUM_1:32
.= (f + (- h)) + (g + (- k)) by RVSUM_1:32
.= (f - h) + (g + (- k)) by RVSUM_1:52
.= (f - h) + (g - k) by RVSUM_1:52 ; :: thesis: verum