let i be natural Number ; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)
let R1, R2 be Element of i -tuples_on REAL; :: thesis: Sum (R1 - R2) = (Sum R1) - (Sum R2)
thus Sum (R1 - R2) = (Sum R1) + (Sum (- R2)) by Th89
.= (Sum R1) + (- (Sum R2)) by Th88
.= (Sum R1) - (Sum R2) ; :: thesis: verum