Description: Sum over a disjoint indexed union, intersected with a finite set D . Similar to fsumiun , but here A and B need not be finite. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsumiunss.b | |
|
fsumiunss.dj | |
||
fsumiunss.c | |
||
fsumiunss.fi | |
||
Assertion | fsumiunss | |