Group sum operation: alternatives using supp and finSupp
Group sum operation: alternatives using supp and finSupp

- In contrast to the theorems in section "Group sum operation", the definitions
` supp ` for the support of functions and ` finSupp ` for finitely supported
are used.
- Additional theorems for supp and finSupp

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