theorem Th34: :: MEASURE9:36

for F being FinSequence of ExtREAL
for k being Nat holds
( ( F is without-infty implies F | k is without-infty ) & ( F is without+infty implies F | k is without+infty ) )