theorem Th67: :: MEASUR12:67

for R1, R2 being without-infty FinSequence of ExtREAL st R1,R2 are_fiberwise_equipotent holds
Sum R1 = Sum R2