theorem :: RVSUM_1:23

for i being natural Number
for R1, R2 being Element of i -tuples_on REAL st R1 + R2 = i |-> 0 holds
R1 = - R2 by Th8, Th9, BINOP_2:2, FINSEQOP:74;