theorem :: RVSUM_2:37

for i being Nat holds Sum (i |-> 0c) = 0c