theorem Th10: :: NUMERAL2:10

for cF being complex-valued XFinSequence
for B1, B2 being set st B1 misses B2 holds
Sum (SubXFinS (cF,(B1 \/ B2))) = (Sum (SubXFinS (cF,B1))) + (Sum (SubXFinS (cF,B2)))