theorem :: DBLSEQ_2:53

for s1, s2 being Real_Sequence st s1,s2 are_fiberwise_equipotent & s1 is nonnegative & s1 is summable holds
( s2 is summable & Sum s1 = Sum s2 )