theorem :: RVSUM_1:14

for i being natural Number
for r1, r2 being Real holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)