theorem Th4: :: SEQ_2:4

for seq being Real_Sequence
for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(seq . m).| < r ) )