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