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