for n being Nat
for x being sequence of (REAL-NS n) st ex K being Real st
for i being Nat holds ||.(x . i).|| < K holds
ex x0 being subsequence of x st x0 is convergent