Description: The value of a sum over a nonempty finite set. (Contributed by Mario Carneiro, 20-Apr-2014) (Revised by Mario Carneiro, 13-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsum.1 | |
|
fsum.2 | |
||
fsum.3 | |
||
fsum.4 | |
||
fsum.5 | |
||
Assertion | fsum | |