let seq be ExtREAL_sequence; :: thesis: ( seq is convergent_to_finite_number implies ex k being Nat st seq ^\ k is bounded )

assume A1: seq is convergent_to_finite_number ; :: thesis: ex k being Nat st seq ^\ k is bounded

then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50;

A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51;

seq is convergent by A1, MESFUNC5:def 11;

then A4: ex g being Real st

( lim seq = g & ( for p being Real 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 such that

A5: lim seq = g ;

reconsider jj = 1 as Real ;

set UB = g + jj;

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 12;

take K ; :: thesis: seq ^\ K is bounded

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;

hence rng (seq ^\ K) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum

assume A1: seq is convergent_to_finite_number ; :: thesis: ex k being Nat st seq ^\ k is bounded

then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50;

A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51;

seq is convergent by A1, MESFUNC5:def 11;

then A4: ex g being Real st

( lim seq = g & ( for p being Real 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 such that

A5: lim seq = g ;

reconsider jj = 1 as Real ;

set UB = g + jj;

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 12;

take K ; :: thesis: seq ^\ K is bounded

now :: thesis: for r being ExtReal st r in rng (seq ^\ K) holds

r <= g + jj

then
g + jj is UpperBound of rng (seq ^\ K)
by XXREAL_2:def 1;r <= g + jj

let r be ExtReal; :: thesis: ( r in rng (seq ^\ K) implies r <= g + jj )

assume r in rng (seq ^\ K) ; :: thesis: r <= g + jj

then consider n being object such that

A7: n in dom (seq ^\ K) and

A8: r = (seq ^\ K) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A7;

|.((seq . (n + k)) - (lim seq)).| <= 1. by A6, NAT_1:11;

then (seq . (n + k)) - (lim seq) <= 1. by EXTREAL1:23;

then ((seq . (n + k)) + (- (lim seq))) + (lim seq) <= 1. + (lim seq) by XXREAL_3:36;

then (seq . (n + k)) + ((- (lim seq)) + (lim seq)) <= 1. + (lim seq) by A5, XXREAL_3:29;

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 + jj by A5, SUPINF_2:1;

hence r <= g + jj by A8, NAT_1:def 3; :: thesis: verum

end;assume r in rng (seq ^\ K) ; :: thesis: r <= g + jj

then consider n being object such that

A7: n in dom (seq ^\ K) and

A8: r = (seq ^\ K) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A7;

|.((seq . (n + k)) - (lim seq)).| <= 1. by A6, NAT_1:11;

then (seq . (n + k)) - (lim seq) <= 1. by EXTREAL1:23;

then ((seq . (n + k)) + (- (lim seq))) + (lim seq) <= 1. + (lim seq) by XXREAL_3:36;

then (seq . (n + k)) + ((- (lim seq)) + (lim seq)) <= 1. + (lim seq) by A5, XXREAL_3:29;

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 + jj by A5, SUPINF_2:1;

hence r <= g + jj by A8, NAT_1:def 3; :: thesis: verum

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 :: thesis: for r being ExtReal st r in rng (seq ^\ K) holds

g - 1 <= r

then
g - 1 is LowerBound of rng (seq ^\ K)
by XXREAL_2:def 2;g - 1 <= r

let r be ExtReal; :: thesis: ( r in rng (seq ^\ K) implies g - 1 <= r )

assume r in rng (seq ^\ K) ; :: thesis: g - 1 <= r

then consider n being object such that

A9: n in dom (seq ^\ K) and

A10: r = (seq ^\ K) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A9;

|.((seq . (n + k)) - (lim seq)).| < 1 by A6, NAT_1:11;

then - 1. <= (seq . (n + k)) - (lim seq) by EXTREAL1:23;

then (- 1.) + (lim seq) <= ((seq . (n + k)) + (- (lim seq))) + (lim seq) by XXREAL_3:36;

then (- 1.) + (lim seq) <= (seq . (n + k)) + ((- (lim seq)) + (lim seq)) by A5, XXREAL_3:29;

then A11: (- 1.) + (lim seq) <= (seq . (n + k)) + 0. by XXREAL_3:7;

- 1. = - jj by SUPINF_2:2;

then (- jj) + g = (- 1.) + (lim seq) by A5, SUPINF_2:1;

then g - 1 <= seq . (n + k) by A11, XXREAL_3:4;

hence g - 1 <= r by A10, NAT_1:def 3; :: thesis: verum

end;assume r in rng (seq ^\ K) ; :: thesis: g - 1 <= r

then consider n being object such that

A9: n in dom (seq ^\ K) and

A10: r = (seq ^\ K) . n by FUNCT_1:def 3;

reconsider n = n as Element of NAT by A9;

|.((seq . (n + k)) - (lim seq)).| < 1 by A6, NAT_1:11;

then - 1. <= (seq . (n + k)) - (lim seq) by EXTREAL1:23;

then (- 1.) + (lim seq) <= ((seq . (n + k)) + (- (lim seq))) + (lim seq) by XXREAL_3:36;

then (- 1.) + (lim seq) <= (seq . (n + k)) + ((- (lim seq)) + (lim seq)) by A5, XXREAL_3:29;

then A11: (- 1.) + (lim seq) <= (seq . (n + k)) + 0. by XXREAL_3:7;

- 1. = - jj by SUPINF_2:2;

then (- jj) + g = (- 1.) + (lim seq) by A5, SUPINF_2:1;

then g - 1 <= seq . (n + k) by A11, XXREAL_3:4;

hence g - 1 <= r by A10, NAT_1:def 3; :: thesis: verum

hence rng (seq ^\ K) is bounded_below by XXREAL_2:def 9; :: according to RINFSUP2:def 3 :: thesis: verum