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