theorem Th89: :: RVSUM_1:89

for i being natural Number
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)