Add summation to iset.mm
Add summation to iset.mm

This is the syntax sum_ and definition df-sum . They are copied
without change from set.mm. Although there are aspects of this
definition that won't work quite the same without excluded middle,
I don't think there is a need to change the definition.

metamath/set.mm,metamath/set.mm,metamath/set.mm