Description: Closure of a finite group sum. This theorem has a weaker hypothesis
than gsumcl , because it is not required that F is a function
(actually, the hypothesis always holds for any proper class F ).
(Contributed by Mario Carneiro, 15-Dec-2014)(Revised by Mario
Carneiro, 24-Apr-2016)(Revised by AV, 3-Jun-2019)