Description: Re-index an infinite group sum using a bijection. (Contributed by Mario Carneiro, 18-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tsmsf1o.b | |
|
tsmsf1o.1 | |
||
tsmsf1o.2 | |
||
tsmsf1o.a | |
||
tsmsf1o.f | |
||
tsmsf1o.s | |
||
Assertion | tsmsf1o | |