Description: Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0f1o.1 | |
|
sge0f1o.2 | |
||
sge0f1o.3 | |
||
sge0f1o.4 | |
||
sge0f1o.5 | |
||
sge0f1o.6 | |
||
sge0f1o.7 | |
||
Assertion | sge0f1o | |