theorem Th81: :: RVSUM_1:81

for i being natural Number holds Sum (i |-> 0) = 0