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