theorem :: MEASURE9:38

for F being V251() FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
( G is summable & Sum F = Sum G )