theorem Th90: :: RVSUM_1:90
for i being natural Number
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)