let i be Nat; :: thesis: Sum (i |-> 0c ) = 0c
thus Sum (i |-> 0c ) = i * 0 by Th110
.= 0c ; :: thesis: verum