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