Add fsumadd to iset.mm
Add fsumadd to iset.mm

The theorem is stated as in set.mm. The proof is basically the set.mm
one but many steps need to be changed for decidability, differences in
seq , closure , and the like.

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