Description: Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sge0fodjrnlem.k | |
|
sge0fodjrnlem.n | |
||
sge0fodjrnlem.bd | |
||
sge0fodjrnlem.c | |
||
sge0fodjrnlem.f | |
||
sge0fodjrnlem.dj | |
||
sge0fodjrnlem.fng | |
||
sge0fodjrnlem.b | |
||
sge0fodjrnlem.b0 | |
||
sge0fodjrnlem.z | |
||
Assertion | sge0fodjrnlem | |