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: seq is convergent by MESFUNC5:def 11;
( ( not lim seq = +infty or not seq is convergent_to_+infty ) & ( not lim seq = -infty or not seq is convergent_to_-infty ) ) by A1, MESFUNC5:56, MESFUNC5:57;
then A3: 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, MESFUNC5:def 12;
then consider g being real number such that
A4: lim seq = g ;
consider k being Nat such that
A5: for m being Nat st k <= m holds
|.((seq . m) - (lim seq)).| < 1 by A3;
A6: g is Real by XREAL_0:def 1;
then A7: - (lim seq) = - g by A4, SUPINF_2:3;
reconsider K = k as Element of NAT by ORDINAL1:def 13;
take K ; :: thesis: seq ^\ K is bounded
set UB = g + 1;
set UL = g - 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) & 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 A5, 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 A4, A7, 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 A4, A6, SUPINF_2:1;
hence r <= g + 1 by A8, 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 SUPINF_1:def 11; :: according to RINFSUP2:def 4,RINFSUP2:def 5 :: thesis: seq ^\ K is bounded_below

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
A9: ( n in dom (seq ^\ K) & r = (seq ^\ K) . n ) by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A9;
|.((seq . (n + k)) - (lim seq)).| < 1 by A5, 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 A4, A7, XXREAL_3:30;
then A10: (- 1. ) + (lim seq) <= (seq . (n + k)) + 0. by XXREAL_3:7;
- 1. = - 1 by SUPINF_2:3;
then (- 1) + g = (- 1. ) + (lim seq) by A4, A6, SUPINF_2:1;
then g - 1 <= seq . (n + k) by A10, XXREAL_3:4;
hence g - 1 <= r by A9, 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 SUPINF_1:def 12; :: according to RINFSUP2:def 3 :: thesis: verum