let seq be ExtREAL_sequence; :: thesis: ( seq is convergent_to_finite_number implies ex k being Element of NAT st seq ^\ k is bounded )
assume A1: seq is convergent_to_finite_number ; :: thesis: ex k being Element of NAT st seq ^\ k is bounded
then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:56;
A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:57;
seq is convergent by A1, MESFUNC5:def 11;
then A4: ex g being real number st
( lim seq = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def 12;
then consider g being real number such that
A5: lim seq = g ;
set UB = g + 1;
consider k being Nat such that
A6: for m being Nat st k <= m holds
|.((seq . m) - (lim seq)).| < 1 by A4;
reconsider K = k as Element of NAT by ORDINAL1:def 13;
take K ; :: thesis: seq ^\ K is bounded
A7: g is Real by XREAL_0:def 1;

now

let r be ext-real number ; :: thesis: ( r in rng (seq ^\ K) implies r <= g + 1 )
assume r in rng (seq ^\ K) ; :: thesis: r <= g + 1
then consider n being set such that
A8: n in dom (seq ^\ K) and
A9: r = (seq ^\ K) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A8;
|.((seq . (n + k)) - (lim seq)).| <= 1. by A6, NAT_1:11;
then (seq . (n + k)) - (lim seq) <= 1. by EXTREAL2:60;
then ((seq . (n + k)) + (- (lim seq))) + (lim seq) <= 1. + (lim seq) by XXREAL_3:38;
then (seq . (n + k)) + ((- (lim seq)) + (lim seq)) <= 1. + (lim seq) by A5, XXREAL_3:30;
then (seq . (n + k)) + 0. <= 1. + (lim seq) by XXREAL_3:7;
then seq . (n + k) <= 1. + (lim seq) by XXREAL_3:4;
then seq . (n + k) <= g + 1 by A5, A7, SUPINF_2:1;
hence r <= g + 1 by A9, NAT_1:def 3; :: thesis: verum

end;

then g + 1 is UpperBound of rng (seq ^\ K) by XXREAL_2:def 1;
hence rng (seq ^\ K) is bounded_above by XXREAL_2:def 10; :: according to RINFSUP2:def 4,RINFSUP2:def 5 :: thesis: seq ^\ K is bounded_below
set UL = g - 1;

now

let r be ext-real number ; :: thesis: ( r in rng (seq ^\ K) implies g - 1 <= r )
assume r in rng (seq ^\ K) ; :: thesis: g - 1 <= r
then consider n being set such that
A10: n in dom (seq ^\ K) and
A11: r = (seq ^\ K) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A10;
|.((seq . (n + k)) - (lim seq)).| < 1 by A6, NAT_1:11;
then - 1. <= (seq . (n + k)) - (lim seq) by EXTREAL2:60;
then (- 1. ) + (lim seq) <= ((seq . (n + k)) + (- (lim seq))) + (lim seq) by XXREAL_3:38;
then (- 1. ) + (lim seq) <= (seq . (n + k)) + ((- (lim seq)) + (lim seq)) by A5, XXREAL_3:30;
then A12: (- 1. ) + (lim seq) <= (seq . (n + k)) + 0. by XXREAL_3:7;
- 1. = - 1 by SUPINF_2:3;
then (- 1) + g = (- 1. ) + (lim seq) by A5, A7, SUPINF_2:1;
then g - 1 <= seq . (n + k) by A12, XXREAL_3:4;
hence g - 1 <= r by A11, NAT_1:def 3; :: thesis: verum

end;

then g - 1 is LowerBound of rng (seq ^\ K) by XXREAL_2:def 2;
hence rng (seq ^\ K) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum