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