theorem :: RVSUM_1:22

for i being natural Number
for R being Element of i -tuples_on REAL holds R + (- R) = i |-> 0 by Th8, Th9, BINOP_2:2, FINSEQOP:73;