theorem :: RVSUM_1:16

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