Add nfsum1 to iset.mm
Add nfsum1 to iset.mm

This is taken from set.mm with a few changes for the syntax of seq and
some minor differences in nf* theorems.

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