theorem :: TOPRNS_1:44

for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
seq is bounded