:: RINFSUP1 semantic presentation

begin

                Lm1:  for r1, r2, s being real number st 0 < s & r1 <= r2 holds
( r1 < r2 + s & r1 - s < r2 )
proof
let r1, r2, s be real number ; ::_thesis: ( 0 < s & r1 <= r2 implies ( r1 < r2 + s & r1 - s < r2 ) )
assume A1: 0 < s ; ::_thesis: ( not r1 <= r2 or ( r1 < r2 + s & r1 - s < r2 ) )
assume  r1 <= r2 ; ::_thesis: ( r1 < r2 + s & r1 - s < r2 )
then  r1 + 0 < r2 + s by A1, XREAL_1:8;
hence  ( r1 < r2 + s & r1 - s < r2 ) by XREAL_1:19; ::_thesis: verum
end;

theorem Th1: :: RINFSUP1:1
for s, r, t being real number holds
( ( s - r < t & s + r > t ) iff abs (t - s) < r )
proof
let s, r, t be real number ; ::_thesis: ( ( s - r < t & s + r > t ) iff abs (t - s) < r )
thus  ( s - r < t & s + r > t implies abs (t - s) < r ) ::_thesis: ( abs (t - s) < r implies ( s - r < t & s + r > t ) )
proof
assume that
A1: s - r < t and
A2: s + r > t ; ::_thesis: abs (t - s) < r
 (- r) + s < t by A1;
then A3: - r < t - s by XREAL_1:20;
 t - s < r by A2, XREAL_1:19;
hence  abs (t - s) < r by A3, SEQ_2:1; ::_thesis: verum
end;
assume A4: abs (t - s) < r ; ::_thesis: ( s - r < t & s + r > t )
then  - r < t - s by SEQ_2:1;
then A5: s + (- r) < t by XREAL_1:20;
 t - s < r by A4, SEQ_2:1;
hence  ( s - r < t & s + r > t ) by A5, XREAL_1:19; ::_thesis: verum
end;

definition
let seq be Real_Sequence;
func upper_bound seq ->  Real equals :: RINFSUP1:def 1
 upper_bound (rng seq);
coherence
 upper_bound (rng seq) is Real ;
end;

:: deftheorem  defines upper_bound RINFSUP1:def_1_:_
 for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);

definition
let seq be Real_Sequence;
func lower_bound seq ->  Real equals :: RINFSUP1:def 2
 lower_bound (rng seq);
coherence
 lower_bound (rng seq) is Real ;
end;

:: deftheorem  defines lower_bound RINFSUP1:def_2_:_
 for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);

theorem Th2: :: RINFSUP1:2
for seq1, seq2 being Real_Sequence holds (seq1 + seq2) - seq2 = seq1
proof
let seq1, seq2 be Real_Sequence; ::_thesis: (seq1 + seq2) - seq2 = seq1
 for n being Element of NAT holds ((seq1 + seq2) - seq2) . n = seq1 . n
proof
let n be Element of NAT ; ::_thesis: ((seq1 + seq2) - seq2) . n = seq1 . n
((seq1 + seq2) - seq2) . n = (seq1 + (seq2 - seq2)) . n by SEQ_1:31
.= (seq1 . n) + ((seq2 + (- seq2)) . n) by SEQ_1:7
.= (seq1 . n) + ((seq2 . n) + ((- seq2) . n)) by SEQ_1:7
.= (seq1 . n) + ((seq2 . n) + (- (seq2 . n))) by SEQ_1:10
.= seq1 . n ;
hence  ((seq1 + seq2) - seq2) . n = seq1 . n ; ::_thesis: verum
end;
hence  (seq1 + seq2) - seq2 = seq1 by FUNCT_2:63; ::_thesis: verum
end;

theorem Th3: :: RINFSUP1:3
for r being real number
for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )
let seq be Real_Sequence; ::_thesis: ( r in rng seq iff - r in rng (- seq) )
thus  ( r in rng seq implies - r in rng (- seq) ) ::_thesis: ( - r in rng (- seq) implies r in rng seq )
proof
assume  r in rng seq ; ::_thesis: - r in rng (- seq)
then consider n being Element of NAT  such that
A1: r = seq . n by FUNCT_2:113;
 - r = (- seq) . n by A1, SEQ_1:10;
hence  - r in rng (- seq) by VALUED_0:28; ::_thesis: verum
end;
assume  - r in rng (- seq) ; ::_thesis: r in rng seq
then consider n being Element of NAT  such that
A2: - r = (- seq) . n by FUNCT_2:113;
 r = - ((- seq) . n) by A2;
then  r = - (- (seq . n)) by SEQ_1:10;
hence  r in rng seq by VALUED_0:28; ::_thesis: verum
end;

theorem Th4: :: RINFSUP1:4
for seq being Real_Sequence holds rng (- seq) = -- (rng seq)
proof
let seq be Real_Sequence; ::_thesis: rng (- seq) = -- (rng seq)
thus  rng (- seq) c= -- (rng seq) :: according to XBOOLE_0:def_10 ::_thesis: -- (rng seq) c= rng (- seq)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (- seq) or x in -- (rng seq) )
assume A1: x in rng (- seq) ; ::_thesis: x in -- (rng seq)
then reconsider r = x as Real ;
 - r in rng (- (- seq)) by A1, Th3;
then  - (- r) in -- (rng seq) by MEASURE6:40;
hence  x in -- (rng seq) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in -- (rng seq) or x in rng (- seq) )
A2: -- (rng seq) c= REAL by MEMBERED:3;
assume A3: x in -- (rng seq) ; ::_thesis: x in rng (- seq)
then reconsider r = x as Real by A2;
 - r in -- (-- (rng seq)) by A3, MEMBER_1:12;
then  - (- r) in rng (- seq) by Th3;
hence  x in rng (- seq) ; ::_thesis: verum
end;

theorem Th5: :: RINFSUP1:5
for seq being Real_Sequence holds
( seq is V88() iff rng seq is bounded_above )
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() iff rng seq is bounded_above )
A1: ( seq is V88() implies rng seq is bounded_above )
proof
assume  seq is V88() ; ::_thesis: rng seq is bounded_above
then consider t being real number  such that
A2: for n being Element of NAT holds seq . n < t by SEQ_2:def_3;
 t is UpperBound of rng seq
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in rng seq or r <= t )
assume  r in rng seq ; ::_thesis: r <= t
then  ex n being set st
( n in dom seq & seq . n = r ) by FUNCT_1:def_3;
hence  r <= t by A2; ::_thesis: verum
end;
hence  rng seq is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
 ( rng seq is bounded_above implies seq is V88() )
proof
assume  rng seq is bounded_above ; ::_thesis: seq is V88()
then consider t being real number  such that
A3: t is UpperBound of rng seq by XXREAL_2:def_10;
A4: for r being real number st r in rng seq holds
r <= t by A3, XXREAL_2:def_1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<_t_+_1
let n be Element of NAT ; ::_thesis: seq . n < t + 1
 seq . n <= t by A4, FUNCT_2:4;
hence  seq . n < t + 1 by Lm1; ::_thesis: verum
end;
hence  seq is V88() by SEQ_2:def_3; ::_thesis: verum
end;
hence  ( seq is V88() iff rng seq is bounded_above ) by A1; ::_thesis: verum
end;

theorem Th6: :: RINFSUP1:6
for seq being Real_Sequence holds
( seq is V89() iff rng seq is bounded_below )
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() iff rng seq is bounded_below )
A1: ( seq is V89() implies rng seq is bounded_below )
proof
assume  seq is V89() ; ::_thesis: rng seq is bounded_below
then consider t being real number  such that
A2: for n being Element of NAT holds t < seq . n by SEQ_2:def_4;
 t is LowerBound of rng seq
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in rng seq or t <= r )
assume  r in rng seq ; ::_thesis: t <= r
then  ex n being set st
( n in dom seq & seq . n = r ) by FUNCT_1:def_3;
hence  t <= r by A2; ::_thesis: verum
end;
hence  rng seq is bounded_below by XXREAL_2:def_9; ::_thesis: verum
end;
 ( rng seq is bounded_below implies seq is V89() )
proof
assume  rng seq is bounded_below ; ::_thesis: seq is V89()
then consider t being real number  such that
A3: t is LowerBound of rng seq by XXREAL_2:def_9;
A4: for r being real number st r in rng seq holds
t <= r by A3, XXREAL_2:def_2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_t_-_1_<_seq_._n
let n be Element of NAT ; ::_thesis: t - 1 < seq . n
 t <= seq . n by A4, FUNCT_2:4;
hence  t - 1 < seq . n by Lm1; ::_thesis: verum
end;
hence  seq is V89() by SEQ_2:def_4; ::_thesis: verum
end;
hence  ( seq is V89() iff rng seq is bounded_below ) by A1; ::_thesis: verum
end;

theorem Th7: :: RINFSUP1:7
for r being real number
for seq being Real_Sequence st seq is V88() holds
( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) ) )
set R = rng seq;
assume  seq is V88() ; ::_thesis: ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
then A1: rng seq is bounded_above by Th5;
A2: rng seq <> {} by RELAT_1:41;
A3: ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) implies r = upper_bound seq )
proof
assume that
A4: for n being Element of NAT holds seq . n <= r and
A5: for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ; ::_thesis: r = upper_bound seq
A6: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r2_being_real_number_st_
(_r2_in_rng_seq_&_r_-_s_<_r2_)
let s be real number ; ::_thesis: ( 0 < s implies ex r2 being real number st
( r2 in rng seq & r - s < r2 ) )
assume  0 < s ; ::_thesis: ex r2 being real number st
( r2 in rng seq & r - s < r2 )
then consider k being Element of NAT  such that
A7: r - s < seq . k by A5;
consider r2 being real number  such that
A8: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:4;
take r2 = r2; ::_thesis: ( r2 in rng seq & r - s < r2 )
thus  ( r2 in rng seq & r - s < r2 ) by A7, A8; ::_thesis: verum
end;
now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_seq_holds_
r1_<=_r
let r1 be real number ; ::_thesis: ( r1 in rng seq implies r1 <= r )
assume  r1 in rng seq ; ::_thesis: r1 <= r
then  ex n being set st
( n in dom seq & seq . n = r1 ) by FUNCT_1:def_3;
hence  r1 <= r by A4; ::_thesis: verum
end;
hence  r = upper_bound seq by A1, A2, A6, SEQ_4:def_1; ::_thesis: verum
end;
 ( r = upper_bound seq implies ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) )
proof
assume A9: r = upper_bound seq ; ::_thesis: ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) )
A10: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_r_-_s_<_seq_._k
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st r - s < seq . k )
assume  0 < s ; ::_thesis: ex k being Element of NAT st r - s < seq . k
then consider r2 being real number  such that
A11: r2 in rng seq and
A12: r - s < r2 by A1, A2, A9, SEQ_4:def_1;
consider k being Element of NAT  such that
A13: r2 = seq . k by A11, SETLIM_1:4;
take k = k; ::_thesis: r - s < seq . k
thus  r - s < seq . k by A12, A13; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<=_r
let n be Element of NAT ; ::_thesis: seq . n <= r
 seq . n in rng seq by FUNCT_2:4;
hence  seq . n <= r by A1, A9, SEQ_4:def_1; ::_thesis: verum
end;
hence  ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) by A10; ::_thesis: verum
end;
hence  ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . k ) ) ) by A3; ::_thesis: verum
end;

theorem Th8: :: RINFSUP1:8
for r being real number
for seq being Real_Sequence st seq is V89() holds
( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) ) )
set R = rng seq;
assume  seq is V89() ; ::_thesis: ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
then A1: rng seq is bounded_below by Th6;
A2: rng seq <> {} by RELAT_1:41;
A3: ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) implies r = lower_bound seq )
proof
assume that
A4: for n being Element of NAT holds r <= seq . n and
A5: for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ; ::_thesis: r = lower_bound seq
A6: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r2_being_real_number_st_
(_r2_in_rng_seq_&_r2_<_r_+_s_)
let s be real number ; ::_thesis: ( 0 < s implies ex r2 being real number st
( r2 in rng seq & r2 < r + s ) )
assume  0 < s ; ::_thesis: ex r2 being real number st
( r2 in rng seq & r2 < r + s )
then consider k being Element of NAT  such that
A7: seq . k < r + s by A5;
consider r2 being real number  such that
A8: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:4;
take r2 = r2; ::_thesis: ( r2 in rng seq & r2 < r + s )
thus  ( r2 in rng seq & r2 < r + s ) by A7, A8; ::_thesis: verum
end;
now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_seq_holds_
r_<=_r1
let r1 be real number ; ::_thesis: ( r1 in rng seq implies r <= r1 )
assume  r1 in rng seq ; ::_thesis: r <= r1
then  ex n being set st
( n in dom seq & seq . n = r1 ) by FUNCT_1:def_3;
hence  r <= r1 by A4; ::_thesis: verum
end;
hence  r = lower_bound seq by A1, A2, A6, SEQ_4:def_2; ::_thesis: verum
end;
 ( r = lower_bound seq implies ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) )
proof
assume A9: r = lower_bound seq ; ::_thesis: ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) )
A10: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_seq_._k_<_r_+_s
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st seq . k < r + s )
assume  0 < s ; ::_thesis: ex k being Element of NAT st seq . k < r + s
then consider r2 being real number  such that
A11: r2 in rng seq and
A12: r2 < r + s by A1, A2, A9, SEQ_4:def_2;
consider k being Element of NAT  such that
A13: r2 = seq . k by A11, SETLIM_1:4;
take k = k; ::_thesis: seq . k < r + s
thus  seq . k < r + s by A12, A13; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_seq_._n
let n be Element of NAT ; ::_thesis: r <= seq . n
 seq . n in rng seq by FUNCT_2:4;
hence  r <= seq . n by A1, A9, SEQ_4:def_2; ::_thesis: verum
end;
hence  ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) by A10; ::_thesis: verum
end;
hence  ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . k < r + s ) ) ) by A3; ::_thesis: verum
end;

theorem Th9: :: RINFSUP1:9
for r being real number
for seq being Real_Sequence holds
( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence holds
( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) )
let seq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) )
thus  ( ( for n being Element of NAT holds seq . n <= r ) implies ( seq is V88() & upper_bound seq <= r ) ) ::_thesis: ( seq is V88() & upper_bound seq <= r implies for n being Element of NAT holds seq . n <= r )
proof
assume A1: for n being Element of NAT holds seq . n <= r ; ::_thesis: ( seq is V88() & upper_bound seq <= r )
now__::_thesis:_for_m_being_Element_of_NAT_holds_seq_._m_<_r_+_1
let m be Element of NAT ; ::_thesis: seq . m < r + 1
 seq . m <= r by A1;
hence  seq . m < r + 1 by Lm1; ::_thesis: verum
end;
hence A2: seq is V88() by SEQ_2:def_3; ::_thesis: upper_bound seq <= r
now__::_thesis:_not_r_<_upper_bound_seq
set r1 = (upper_bound seq) - r;
assume  r < upper_bound seq ; ::_thesis: contradiction
then  (upper_bound seq) - r > 0 by XREAL_1:50;
then  ex k being Element of NAT st (upper_bound seq) - ((upper_bound seq) - r) < seq . k by A2, Th7;
hence  contradiction by A1; ::_thesis: verum
end;
hence  upper_bound seq <= r ; ::_thesis: verum
end;
assume that
A3: seq is V88() and
A4: upper_bound seq <= r ; ::_thesis: for n being Element of NAT holds seq . n <= r
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<=_r
let n be Element of NAT ; ::_thesis: seq . n <= r
 seq . n <= upper_bound seq by A3, Th7;
hence  seq . n <= r by A4, XXREAL_0:2; ::_thesis: verum
end;
hence  for n being Element of NAT holds seq . n <= r ; ::_thesis: verum
end;

theorem Th10: :: RINFSUP1:10
for r being real number
for seq being Real_Sequence holds
( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence holds
( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) )
let seq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) )
thus  ( ( for n being Element of NAT holds r <= seq . n ) implies ( seq is V89() & r <= lower_bound seq ) ) ::_thesis: ( seq is V89() & r <= lower_bound seq implies for n being Element of NAT holds r <= seq . n )
proof
assume A1: for n being Element of NAT holds r <= seq . n ; ::_thesis: ( seq is V89() & r <= lower_bound seq )
now__::_thesis:_for_m_being_Element_of_NAT_holds_r_-_1_<_seq_._m
let m be Element of NAT ; ::_thesis: r - 1 < seq . m
 r <= seq . m by A1;
hence  r - 1 < seq . m by Lm1; ::_thesis: verum
end;
hence A2: seq is V89() by SEQ_2:def_4; ::_thesis: r <= lower_bound seq
now__::_thesis:_not_r_>_lower_bound_seq
set r1 = r - (lower_bound seq);
assume  r > lower_bound seq ; ::_thesis: contradiction
then  r - (lower_bound seq) > 0 by XREAL_1:50;
then  ex k being Element of NAT st seq . k < (lower_bound seq) + (r - (lower_bound seq)) by A2, Th8;
hence  contradiction by A1; ::_thesis: verum
end;
hence  r <= lower_bound seq ; ::_thesis: verum
end;
assume that
A3: seq is V89() and
A4: r <= lower_bound seq ; ::_thesis: for n being Element of NAT holds r <= seq . n
now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_seq_._n
let n be Element of NAT ; ::_thesis: r <= seq . n
 lower_bound seq <= seq . n by A3, Th8;
hence  r <= seq . n by A4, XXREAL_0:2; ::_thesis: verum
end;
hence  for n being Element of NAT holds r <= seq . n ; ::_thesis: verum
end;

theorem :: RINFSUP1:11
for seq being Real_Sequence holds
( seq is V88() iff - seq is V89() )
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() iff - seq is V89() )
set seq1 = - seq;
thus  ( seq is V88() implies - seq is V89() ) ; ::_thesis: ( - seq is V89() implies seq is V88() )
assume  - seq is V89() ; ::_thesis: seq is V88()
then consider t being real number  such that
A1: for n being Element of NAT holds (- seq) . n > t by SEQ_2:def_4;
 for n being Element of NAT holds seq . n < - t
proof
let n be Element of NAT ; ::_thesis: seq . n < - t
 (- seq) . n = - (seq . n) by SEQ_1:10;
then A2: - ((- seq) . n) = seq . n ;
 (- seq) . n > t by A1;
hence  seq . n < - t by A2, XREAL_1:24; ::_thesis: verum
end;
hence  seq is V88() by SEQ_2:def_3; ::_thesis: verum
end;

theorem :: RINFSUP1:12
for seq being Real_Sequence holds
( seq is V89() iff - seq is V88() )
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() iff - seq is V88() )
 - (- seq) = seq ;
hence  ( seq is V89() iff - seq is V88() ) ; ::_thesis: verum
end;

theorem Th13: :: RINFSUP1:13
for seq being Real_Sequence st seq is V88() holds
upper_bound seq = - (lower_bound (- seq))
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies upper_bound seq = - (lower_bound (- seq)) )
assume  seq is V88() ; ::_thesis: upper_bound seq = - (lower_bound (- seq))
then  ( not rng seq is empty & rng seq is bounded_above ) by Th5, RELAT_1:41;
then  upper_bound (rng seq) = - (lower_bound (-- (rng seq))) by MEASURE6:44
.= - (lower_bound (rng (- seq))) by Th4 ;
hence  upper_bound seq = - (lower_bound (- seq)) ; ::_thesis: verum
end;

theorem Th14: :: RINFSUP1:14
for seq being Real_Sequence st seq is V89() holds
lower_bound seq = - (upper_bound (- seq))
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies lower_bound seq = - (upper_bound (- seq)) )
assume  seq is V89() ; ::_thesis: lower_bound seq = - (upper_bound (- seq))
then  ( not rng seq is empty & rng seq is bounded_below ) by Th6, RELAT_1:41;
then  lower_bound (rng seq) = - (upper_bound (-- (rng seq))) by MEASURE6:43
.= - (upper_bound (rng (- seq))) by Th4 ;
hence  lower_bound seq = - (upper_bound (- seq)) ; ::_thesis: verum
end;

theorem Th15: :: RINFSUP1:15
for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds
lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq2 is V89() implies lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2) )
assume that
A1: seq1 is V89() and
A2: seq2 is V89() ; ::_thesis: lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2)
 for n being Element of NAT holds (seq1 + seq2) . n >= (lower_bound seq1) + (lower_bound seq2)
proof
let n be Element of NAT ; ::_thesis: (seq1 + seq2) . n >= (lower_bound seq1) + (lower_bound seq2)
A3: seq2 . n >= lower_bound seq2 by A2, Th8;
 ( (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) & seq1 . n >= lower_bound seq1 ) by A1, Th8, SEQ_1:7;
hence  (seq1 + seq2) . n >= (lower_bound seq1) + (lower_bound seq2) by A3, XREAL_1:7; ::_thesis: verum
end;
hence  lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2) by Th10; ::_thesis: verum
end;

theorem Th16: :: RINFSUP1:16
for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds
upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq2 is V88() implies upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) )
assume that
A1: seq1 is V88() and
A2: seq2 is V88() ; ::_thesis: upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2)
 for n being Element of NAT holds (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2)
proof
let n be Element of NAT ; ::_thesis: (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2)
A3: seq2 . n <= upper_bound seq2 by A2, Th7;
 ( (seq1 + seq2) . n = (seq1 . n) + (seq2 . n) & seq1 . n <= upper_bound seq1 ) by A1, Th7, SEQ_1:7;
hence  (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2) by A3, XREAL_1:7; ::_thesis: verum
end;
hence  upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) by Th9; ::_thesis: verum
end;

notation
let f be Real_Sequence;
synonym  nonnegative f for  nonnegative-yielding ;
end;

definition
let f be Real_Sequence;
redefine attr f is nonnegative-yielding  means :Def3: :: RINFSUP1:def 3
 for n being Element of NAT holds f . n >= 0 ;
compatibility
 ( f is nonnegative iff for n being Element of NAT holds f . n >= 0 )
proof
hereby  ::_thesis: ( ( for n being Element of NAT holds f . n >= 0 ) implies f is nonnegative )
assume A1: f is nonnegative ; ::_thesis: for n being Element of NAT holds f . n >= 0
let n be Element of NAT ; ::_thesis: f . n >= 0
 f . n in rng f by VALUED_0:28;
hence  f . n >= 0 by A1, PARTFUN3:def_4; ::_thesis: verum
end;
assume A2: for n being Element of NAT holds f . n >= 0 ; ::_thesis: f is nonnegative
let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( not r in K87(f) or 0 <= r )
assume  r in rng f ; ::_thesis: 0 <= r
then  ex x being Element of NAT st r = f . x by FUNCT_2:113;
hence  0 <= r by A2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines nonnegative RINFSUP1:def_3_:_
 for f being Real_Sequence holds
( f is nonnegative iff for n being Element of NAT holds f . n >= 0 );

theorem Th17: :: RINFSUP1:17
for k being Element of NAT
for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative
proof
let k be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is nonnegative holds
seq ^\ k is nonnegative
let seq be Real_Sequence; ::_thesis: ( seq is nonnegative implies seq ^\ k is nonnegative )
assume A1: seq is nonnegative ; ::_thesis: seq ^\ k is nonnegative
 for n being Element of NAT holds (seq ^\ k) . n >= 0
proof
let n be Element of NAT ; ::_thesis: (seq ^\ k) . n >= 0
 (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
hence  (seq ^\ k) . n >= 0 by A1, Def3; ::_thesis: verum
end;
hence  seq ^\ k is nonnegative by Def3; ::_thesis: verum
end;

theorem Th18: :: RINFSUP1:18
for seq being Real_Sequence st seq is V89() & seq is nonnegative holds
lower_bound seq >= 0
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() & seq is nonnegative implies lower_bound seq >= 0 )
assume  ( seq is V89() & seq is nonnegative ) ; ::_thesis: lower_bound seq >= 0
then  for n being Element of NAT holds seq . n >= 0 by Def3;
hence  lower_bound seq >= 0 by Th10; ::_thesis: verum
end;

theorem :: RINFSUP1:19
for seq being Real_Sequence st seq is V88() & seq is nonnegative holds
upper_bound seq >= 0
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() & seq is nonnegative implies upper_bound seq >= 0 )
assume A1: ( seq is V88() & seq is nonnegative ) ; ::_thesis: upper_bound seq >= 0
then  seq . 0 <= upper_bound seq by Th7;
hence  upper_bound seq >= 0 by A1, Def3; ::_thesis: verum
end;

theorem Th20: :: RINFSUP1:20
for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds
( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative implies ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) )
assume that
A1: ( seq1 is V89() & seq1 is nonnegative ) and
A2: ( seq2 is V89() & seq2 is nonnegative ) ; ::_thesis: ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) )
 for n being Element of NAT holds (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2)
proof
let n be Element of NAT ; ::_thesis: (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2)
A3: ( (seq1 (#) seq2) . n = (seq1 . n) * (seq2 . n) & seq1 . n >= lower_bound seq1 ) by A1, Th8, SEQ_1:8;
A4: lower_bound seq2 >= 0 by A2, Th18;
 ( seq2 . n >= lower_bound seq2 & lower_bound seq1 >= 0 ) by A1, A2, Th8, Th18;
hence  (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2) by A3, A4, XREAL_1:66; ::_thesis: verum
end;
hence  ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) by Th10; ::_thesis: verum
end;

theorem Th21: :: RINFSUP1:21
for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds
( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative implies ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) ) )
assume that
A1: ( seq1 is V88() & seq1 is nonnegative ) and
A2: ( seq2 is V88() & seq2 is nonnegative ) ; ::_thesis: ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) )
 for n being Element of NAT holds (seq1 (#) seq2) . n <= (upper_bound seq1) * (upper_bound seq2)
proof
let n be Element of NAT ; ::_thesis: (seq1 (#) seq2) . n <= (upper_bound seq1) * (upper_bound seq2)
A3: ( (seq1 (#) seq2) . n = (seq1 . n) * (seq2 . n) & seq1 . n <= upper_bound seq1 ) by A1, Th7, SEQ_1:8;
A4: seq2 . n >= 0 by A2, Def3;
 ( seq2 . n <= upper_bound seq2 & seq1 . n >= 0 ) by A1, A2, Def3, Th7;
hence  (seq1 (#) seq2) . n <= (upper_bound seq1) * (upper_bound seq2) by A3, A4, XREAL_1:66; ::_thesis: verum
end;
hence  ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) ) by Th9; ::_thesis: verum
end;

theorem :: RINFSUP1:22
for seq being Real_Sequence st seq is V48() & seq is V88() holds
seq is bounded ;

theorem :: RINFSUP1:23
for seq being Real_Sequence st seq is V49() & seq is V89() holds
seq is bounded ;

theorem Th24: :: RINFSUP1:24
for seq being Real_Sequence st seq is V48() & seq is V88() holds
lim seq = upper_bound seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies lim seq = upper_bound seq )
assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: lim seq = upper_bound seq
then  for n being Element of NAT holds seq . n <= lim seq by SEQ_4:37;
then A2: upper_bound seq <= lim seq by Th9;
 for n being Element of NAT holds seq . n <= upper_bound seq by A1, Th7;
then  lim seq <= upper_bound seq by A1, PREPOWER:2;
hence  lim seq = upper_bound seq by A2, XXREAL_0:1; ::_thesis: verum
end;

theorem Th25: :: RINFSUP1:25
for seq being Real_Sequence st seq is V49() & seq is V89() holds
lim seq = lower_bound seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies lim seq = lower_bound seq )
assume A1: ( seq is V49() & seq is V89() ) ; ::_thesis: lim seq = lower_bound seq
then  for n being Element of NAT holds lim seq <= seq . n by SEQ_4:38;
then A2: lim seq <= lower_bound seq by Th10;
 for n being Element of NAT holds lower_bound seq <= seq . n by A1, Th8;
then  lower_bound seq <= lim seq by A1, PREPOWER:1;
hence  lim seq = lower_bound seq by A2, XXREAL_0:1; ::_thesis: verum
end;

theorem :: RINFSUP1:26
for k being Element of NAT
for seq being Real_Sequence st seq is V88() holds
seq ^\ k is V88() by SEQM_3:27;

theorem :: RINFSUP1:27
for k being Element of NAT
for seq being Real_Sequence st seq is V89() holds
seq ^\ k is V89() by SEQM_3:28;

theorem :: RINFSUP1:28
for k being Element of NAT
for seq being Real_Sequence st seq is bounded holds
seq ^\ k is bounded by SEQM_3:29;

theorem Th29: :: RINFSUP1:29
for seq being Real_Sequence
for n being Element of NAT holds  {  (seq . k) where k is Element of NAT : n <= k  }  is Subset of REAL
proof
let seq be Real_Sequence; ::_thesis: for n being Element of NAT holds  {  (seq . k) where k is Element of NAT : n <= k  }  is Subset of REAL
let n be Element of NAT ; ::_thesis:  {  (seq . k) where k is Element of NAT : n <= k  }  is Subset of REAL
set Y =  {  (seq . k) where k is Element of NAT : n <= k  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
x_in_REAL
let x be set ; ::_thesis: ( x in  {  (seq . k) where k is Element of NAT : n <= k  }  implies x in REAL )
assume  x in  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: x in REAL
then consider z1 being set  such that
A1: z1 = x and
A2: z1 in  {  (seq . k) where k is Element of NAT : n <= k  }  ;
 ex k1 being Element of NAT st
( z1 = seq . k1 & n <= k1 ) by A2;
hence  x in REAL by A1; ::_thesis: verum
end;
hence   {  (seq . k) where k is Element of NAT : n <= k  }  is Subset of REAL by TARSKI:def_3; ::_thesis: verum
end;

theorem Th30: :: RINFSUP1:30
for k being Element of NAT
for seq being Real_Sequence holds rng (seq ^\ k) =  {  (seq . n) where n is Element of NAT : k <= n  }
proof
let k be Element of NAT ; ::_thesis: for seq being Real_Sequence holds rng (seq ^\ k) =  {  (seq . n) where n is Element of NAT : k <= n  }
let seq be Real_Sequence; ::_thesis: rng (seq ^\ k) =  {  (seq . n) where n is Element of NAT : k <= n  }
set seq1 = seq ^\ k;
set Z =  {  (seq . m) where m is Element of NAT : k <= m  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._m)_where_m_is_Element_of_NAT_:_k_<=_m__}__holds_
x_in_rng_(seq_^\_k)
let x be set ; ::_thesis: ( x in  {  (seq . m) where m is Element of NAT : k <= m  }  implies x in rng (seq ^\ k) )
assume  x in  {  (seq . m) where m is Element of NAT : k <= m  }  ; ::_thesis: x in rng (seq ^\ k)
then consider k1 being Element of NAT  such that
A1: x = seq . k1 and
A2: k <= k1 ;
consider k2 being Nat such that
A3: k1 = k + k2 by A2, NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12;
 x = (seq ^\ k) . k2 by A1, A3, NAT_1:def_3;
hence  x in rng (seq ^\ k) by FUNCT_2:4; ::_thesis: verum
end;
then A4:  {  (seq . m) where m is Element of NAT : k <= m  }  c= rng (seq ^\ k) by TARSKI:def_3;
A5: dom (seq ^\ k) = NAT by FUNCT_2:def_1;
now__::_thesis:_for_y_being_set_st_y_in_rng_(seq_^\_k)_holds_
y_in__{__(seq_._m)_where_m_is_Element_of_NAT_:_k_<=_m__}_
let y be set ; ::_thesis: ( y in rng (seq ^\ k) implies y in  {  (seq . m) where m is Element of NAT : k <= m  }  )
assume  y in rng (seq ^\ k) ; ::_thesis: y in  {  (seq . m) where m is Element of NAT : k <= m  }
then consider m1 being set  such that
A6: m1 in NAT and
A7: y = (seq ^\ k) . m1 by A5, FUNCT_1:def_3;
reconsider m1 = m1 as Element of NAT by A6;
 y = seq . (k + m1) by A7, NAT_1:def_3;
hence  y in  {  (seq . m) where m is Element of NAT : k <= m  }  by SETLIM_1:1; ::_thesis: verum
end;
then  rng (seq ^\ k) c=  {  (seq . m) where m is Element of NAT : k <= m  }  by TARSKI:def_3;
hence  rng (seq ^\ k) =  {  (seq . n) where n is Element of NAT : k <= n  }  by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th31: :: RINFSUP1:31
for seq being Real_Sequence st seq is V88() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_above
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_above )
assume A1: seq is V88() ; ::_thesis: for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_above
let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_above
set seq1 = seq ^\ n;
 seq ^\ n is V88() by A1, SEQM_3:27;
then A2: rng (seq ^\ n) is bounded_above by Th5;
let R be Subset of REAL; ::_thesis: ( R =  {  (seq . k) where k is Element of NAT : n <= k  }  implies R is bounded_above )
assume  R =  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: R is bounded_above
hence  R is bounded_above by A2, Th30; ::_thesis: verum
end;

theorem Th32: :: RINFSUP1:32
for seq being Real_Sequence st seq is V89() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_below
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_below )
assume A1: seq is V89() ; ::_thesis: for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_below
let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is bounded_below
set seq1 = seq ^\ n;
 seq ^\ n is V89() by A1, SEQM_3:28;
then A2: rng (seq ^\ n) is bounded_below by Th6;
let R be Subset of REAL; ::_thesis: ( R =  {  (seq . k) where k is Element of NAT : n <= k  }  implies R is bounded_below )
assume  R =  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: R is bounded_below
hence  R is bounded_below by A2, Th30; ::_thesis: verum
end;

theorem Th33: :: RINFSUP1:33
for seq being Real_Sequence st seq is bounded holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is real-bounded
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is real-bounded )
assume A1: seq is bounded ; ::_thesis: for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is real-bounded
let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
R is real-bounded
let R be Subset of REAL; ::_thesis: ( R =  {  (seq . k) where k is Element of NAT : n <= k  }  implies R is real-bounded )
assume  R =  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: R is real-bounded
then  ( R is bounded_above & R is bounded_below ) by A1, Th31, Th32;
hence  R is real-bounded by XXREAL_2:def_11; ::_thesis: verum
end;

theorem Th34: :: RINFSUP1:34
for seq being Real_Sequence st seq is V48() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
lower_bound R = seq . n
proof
let seq be Real_Sequence; ::_thesis: ( seq is V48() implies for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
lower_bound R = seq . n )
assume A1: seq is V48() ; ::_thesis: for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
lower_bound R = seq . n
let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
lower_bound R = seq . n
A2: now__::_thesis:_for_r_being_real_number_st_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
seq_._n_<=_r
let r be real number ; ::_thesis: ( r in  {  (seq . k) where k is Element of NAT : n <= k  }  implies seq . n <= r )
assume  r in  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: seq . n <= r
then consider r1 being real number  such that
A3: ( r = r1 & r1 in  {  (seq . k) where k is Element of NAT : n <= k  }  ) ;
consider k1 being Element of NAT  such that
A4: r1 = seq . k1 and
A5: n <= k1 by A3;
consider k being Nat such that
A6: n + k = k1 by A5, NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  seq . n <= r by A1, A3, A4, A6, SEQM_3:5; ::_thesis: verum
end;
let R be Subset of REAL; ::_thesis: ( R =  {  (seq . k) where k is Element of NAT : n <= k  }  implies lower_bound R = seq . n )
A7: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r_being_real_number_st_
(_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__&_r_<_(seq_._n)_+_s_)
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in  {  (seq . k) where k is Element of NAT : n <= k  }  & r < (seq . n) + s ) )
A8: seq . n in  {  (seq . k) where k is Element of NAT : n <= k  }  ;
assume  0 < s ; ::_thesis: ex r being real number st
( r in  {  (seq . k) where k is Element of NAT : n <= k  }  & r < (seq . n) + s )
hence  ex r being real number st
( r in  {  (seq . k) where k is Element of NAT : n <= k  }  & r < (seq . n) + s ) by A8, XREAL_1:29; ::_thesis: verum
end;
assume A9: R =  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: lower_bound R = seq . n
then A10: R <> {} by SETLIM_1:1;
 R is bounded_below by A1, A9, Th32, LIMFUNC1:1;
hence  lower_bound R = seq . n by A9, A10, A2, A7, SEQ_4:def_2; ::_thesis: verum
end;

theorem Th35: :: RINFSUP1:35
for seq being Real_Sequence st seq is V49() holds
for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
upper_bound R = seq . n
proof
let seq be Real_Sequence; ::_thesis: ( seq is V49() implies for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
upper_bound R = seq . n )
assume A1: seq is V49() ; ::_thesis: for n being Element of NAT
for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
upper_bound R = seq . n
let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
upper_bound R = seq . n
A2: now__::_thesis:_for_r_being_real_number_st_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_
r_<=_seq_._n
let r be real number ; ::_thesis: ( r in  {  (seq . k) where k is Element of NAT : n <= k  }  implies r <= seq . n )
assume  r in  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: r <= seq . n
then consider r1 being real number  such that
A3: ( r = r1 & r1 in  {  (seq . k) where k is Element of NAT : n <= k  }  ) ;
consider k1 being Element of NAT  such that
A4: r1 = seq . k1 and
A5: n <= k1 by A3;
consider k being Nat such that
A6: n + k = k1 by A5, NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  r <= seq . n by A1, A3, A4, A6, SEQM_3:7; ::_thesis: verum
end;
let R be Subset of REAL; ::_thesis: ( R =  {  (seq . k) where k is Element of NAT : n <= k  }  implies upper_bound R = seq . n )
A7: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_r_being_real_number_st_
(_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__&_(seq_._n)_-_s_<_r_)
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in  {  (seq . k) where k is Element of NAT : n <= k  }  & (seq . n) - s < r ) )
A8: seq . n in  {  (seq . k) where k is Element of NAT : n <= k  }  ;
assume  0 < s ; ::_thesis: ex r being real number st
( r in  {  (seq . k) where k is Element of NAT : n <= k  }  & (seq . n) - s < r )
hence  ex r being real number st
( r in  {  (seq . k) where k is Element of NAT : n <= k  }  & (seq . n) - s < r ) by A8, XREAL_1:44; ::_thesis: verum
end;
assume A9: R =  {  (seq . k) where k is Element of NAT : n <= k  }  ; ::_thesis: upper_bound R = seq . n
then A10: R <> {} by SETLIM_1:1;
 R is bounded_above by A1, A9, Th31, LIMFUNC1:1;
hence  upper_bound R = seq . n by A9, A10, A2, A7, SEQ_4:def_1; ::_thesis: verum
end;

definition
let seq be Real_Sequence;
func inferior_realsequence seq ->  Real_Sequence means :Def4: :: RINFSUP1:def 4
 for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
it . n = lower_bound Y;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = lower_bound Y
proof
defpred S1[ Element of NAT , Element of REAL ] means  for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : $1 <= k  }  holds
$2 = lower_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[n,y]
reconsider Y =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
reconsider y = lower_bound Y as Element of REAL ;
 for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
y = lower_bound Y ;
hence  ex y being Element of REAL st S1[n,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,REAL st
for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1);
hence  ex b1 being Real_Sequence st
for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = lower_bound Y ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = lower_bound Y ) & ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = lower_bound Y ) holds
b1 = b2
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
seq1 . n = lower_bound Y ) & ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
seq2 . n = lower_bound Y ) implies seq1 = seq2 )
assume that
A2: for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
seq1 . n = lower_bound Y and
A3: for m being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : m <= k  }  holds
seq2 . m = lower_bound Y ; ::_thesis: seq1 = seq2
A4: for y being set st y in NAT holds
seq1 . y = seq2 . y
proof
let y be set ; ::_thesis: ( y in NAT implies seq1 . y = seq2 . y )
assume  y in NAT ; ::_thesis: seq1 . y = seq2 . y
then reconsider y = y as Element of NAT ;
reconsider Y =  {  (seq . k) where k is Element of NAT : y <= k  }  as Subset of REAL by Th29;
 seq1 . y = lower_bound Y by A2;
hence  seq1 . y = seq2 . y by A3; ::_thesis: verum
end;
 ( NAT = dom seq1 & NAT = dom seq2 ) by FUNCT_2:def_1;
hence  seq1 = seq2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def_4_:_
 for seq, b2 being Real_Sequence holds
( b2 = inferior_realsequence seq iff for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = lower_bound Y );

definition
let seq be Real_Sequence;
func superior_realsequence seq ->  Real_Sequence means :Def5: :: RINFSUP1:def 5
 for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
it . n = upper_bound Y;
existence
 ex b1 being Real_Sequence st
for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = upper_bound Y
proof
defpred S1[ Element of NAT , Element of REAL ] means  for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : $1 <= k  }  holds
$2 = upper_bound Y;
A1: for n being Element of NAT ex y being Element of REAL st S1[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[n,y]
reconsider Y =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
reconsider y = upper_bound Y as Element of REAL ;
 for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
y = upper_bound Y ;
hence  ex y being Element of REAL st S1[n,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,REAL st
for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1);
hence  ex b1 being Real_Sequence st
for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = upper_bound Y ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b1 . n = upper_bound Y ) & ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = upper_bound Y ) holds
b1 = b2
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
seq1 . n = upper_bound Y ) & ( for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
seq2 . n = upper_bound Y ) implies seq1 = seq2 )
assume that
A2: for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
seq1 . n = upper_bound Y and
A3: for m being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : m <= k  }  holds
seq2 . m = upper_bound Y ; ::_thesis: seq1 = seq2
A4: for y being set st y in NAT holds
seq1 . y = seq2 . y
proof
let y be set ; ::_thesis: ( y in NAT implies seq1 . y = seq2 . y )
assume  y in NAT ; ::_thesis: seq1 . y = seq2 . y
then reconsider y = y as Element of NAT ;
reconsider Y =  {  (seq . k) where k is Element of NAT : y <= k  }  as Subset of REAL by Th29;
 seq1 . y = upper_bound Y by A2;
hence  seq1 . y = seq2 . y by A3; ::_thesis: verum
end;
 ( NAT = dom seq1 & NAT = dom seq2 ) by FUNCT_2:def_1;
hence  seq1 = seq2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines superior_realsequence RINFSUP1:def_5_:_
 for seq, b2 being Real_Sequence holds
( b2 = superior_realsequence seq iff for n being Element of NAT
for Y being Subset of REAL st Y =  {  (seq . k) where k is Element of NAT : n <= k  }  holds
b2 . n = upper_bound Y );

theorem Th36: :: RINFSUP1:36
for n being Element of NAT
for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n)
let seq be Real_Sequence; ::_thesis: (inferior_realsequence seq) . n = lower_bound (seq ^\ n)
reconsider Y =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
(inferior_realsequence seq) . n = lower_bound Y by Def4
.= lower_bound (rng (seq ^\ n)) by Th30 ;
hence  (inferior_realsequence seq) . n = lower_bound (seq ^\ n) ; ::_thesis: verum
end;

theorem Th37: :: RINFSUP1:37
for n being Element of NAT
for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n)
let seq be Real_Sequence; ::_thesis: (superior_realsequence seq) . n = upper_bound (seq ^\ n)
reconsider Y =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
(superior_realsequence seq) . n = upper_bound Y by Def5
.= upper_bound (rng (seq ^\ n)) by Th30 ;
hence  (superior_realsequence seq) . n = upper_bound (seq ^\ n) ; ::_thesis: verum
end;

theorem Th38: :: RINFSUP1:38
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . 0 = lower_bound seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . 0 = lower_bound seq )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : 0 <= k  }  as Subset of REAL by Th29;
(inferior_realsequence seq) . 0 = lower_bound Y1 by Def4
.= lower_bound seq by SETLIM_1:5 ;
hence  ( seq is V89() implies (inferior_realsequence seq) . 0 = lower_bound seq ) ; ::_thesis: verum
end;

theorem Th39: :: RINFSUP1:39
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . 0 = upper_bound seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . 0 = upper_bound seq )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : 0 <= k  }  as Subset of REAL by Th29;
(superior_realsequence seq) . 0 = upper_bound Y1 by Def5
.= upper_bound seq by SETLIM_1:5 ;
hence  ( seq is V88() implies (superior_realsequence seq) . 0 = upper_bound seq ) ; ::_thesis: verum
end;

theorem Th40: :: RINFSUP1:40
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V89() holds
( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) )
proof
let n be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence st seq is V89() holds
( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) )
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) )
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) ) )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
assume  seq is V89() ; ::_thesis: ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) )
then A1: ( not Y1 is empty & Y1 is bounded_below ) by Th32, SETLIM_1:1;
thus  ( r = (inferior_realsequence seq) . n implies ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) ) ::_thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) implies r = (inferior_realsequence seq) . n )
proof
assume  r = (inferior_realsequence seq) . n ; ::_thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) )
then A2: r = lower_bound Y1 by Def4;
A3: for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s
proof
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st seq . (n + k) < r + s )
assume  0 < s ; ::_thesis: ex k being Element of NAT st seq . (n + k) < r + s
then consider r1 being real number  such that
A4: r1 in Y1 and
A5: r1 < r + s by A1, A2, SEQ_4:def_2;
consider k1 being Element of NAT  such that
A6: r1 = seq . k1 and
A7: n <= k1 by A4;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
 k2 in NAT by ORDINAL1:def_12;
hence  ex k being Element of NAT st seq . (n + k) < r + s by A5, A6, A8; ::_thesis: verum
end;
 for k being Element of NAT holds r <= seq . (n + k)
proof
let k be Element of NAT ; ::_thesis: r <= seq . (n + k)
 seq . (n + k) in Y1 by SETLIM_1:1;
hence  r <= seq . (n + k) by A1, A2, SEQ_4:def_2; ::_thesis: verum
end;
hence  ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ) ) by A3; ::_thesis: verum
end;
assume that
A9: for k being Element of NAT holds r <= seq . (n + k) and
A10: for s being real number st 0 < s holds
ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: r = (inferior_realsequence seq) . n
A11: for s being real number st 0 < s holds
ex r1 being real number st
( r1 in Y1 & r1 < r + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r1 being real number st
( r1 in Y1 & r1 < r + s ) )
assume  0 < s ; ::_thesis: ex r1 being real number st
( r1 in Y1 & r1 < r + s )
then consider k being Element of NAT  such that
A12: seq . (n + k) < r + s by A10;
 n + k >= n by NAT_1:11;
then  seq . (n + k) in Y1 ;
hence  ex r1 being real number st
( r1 in Y1 & r1 < r + s ) by A12; ::_thesis: verum
end;
 for r1 being real number st r1 in Y1 holds
r <= r1
proof
let r1 be real number ; ::_thesis: ( r1 in Y1 implies r <= r1 )
assume  r1 in Y1 ; ::_thesis: r <= r1
then consider k1 being Element of NAT  such that
A13: r1 = seq . k1 and
A14: n <= k1 ;
consider k2 being Nat such that
A15: k1 = n + k2 by A14, NAT_1:10;
 k2 in NAT by ORDINAL1:def_12;
hence  r <= r1 by A9, A13, A15; ::_thesis: verum
end;
then  r = lower_bound Y1 by A1, A11, SEQ_4:def_2;
hence  r = (inferior_realsequence seq) . n by Def4; ::_thesis: verum
end;

theorem Th41: :: RINFSUP1:41
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V88() holds
( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
proof
let n be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence st seq is V88() holds
( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) ) )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
assume  seq is V88() ; ::_thesis: ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) )
then A1: ( not Y1 is empty & Y1 is bounded_above ) by Th31, SETLIM_1:1;
thus  ( r = (superior_realsequence seq) . n implies ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) ) ::_thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) implies r = (superior_realsequence seq) . n )
proof
assume  r = (superior_realsequence seq) . n ; ::_thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) )
then A2: r = upper_bound Y1 by Def5;
A3: for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k)
proof
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st r - s < seq . (n + k) )
assume  0 < s ; ::_thesis: ex k being Element of NAT st r - s < seq . (n + k)
then consider r1 being real number  such that
A4: r1 in Y1 and
A5: r - s < r1 by A1, A2, SEQ_4:def_1;
consider k1 being Element of NAT  such that
A6: r1 = seq . k1 and
A7: n <= k1 by A4;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
 k2 in NAT by ORDINAL1:def_12;
hence  ex k being Element of NAT st r - s < seq . (n + k) by A5, A6, A8; ::_thesis: verum
end;
 for k being Element of NAT holds seq . (n + k) <= r
proof
let k be Element of NAT ; ::_thesis: seq . (n + k) <= r
 seq . (n + k) in Y1 by SETLIM_1:1;
hence  seq . (n + k) <= r by A1, A2, SEQ_4:def_1; ::_thesis: verum
end;
hence  ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ) ) by A3; ::_thesis: verum
end;
assume that
A9: for k being Element of NAT holds seq . (n + k) <= r and
A10: for s being real number st 0 < s holds
ex k being Element of NAT st r - s < seq . (n + k) ; ::_thesis: r = (superior_realsequence seq) . n
A11: for s being real number st 0 < s holds
ex r1 being real number st
( r1 in Y1 & r - s < r1 )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r1 being real number st
( r1 in Y1 & r - s < r1 ) )
assume  0 < s ; ::_thesis: ex r1 being real number st
( r1 in Y1 & r - s < r1 )
then consider k being Element of NAT  such that
A12: r - s < seq . (n + k) by A10;
 n + k >= n by NAT_1:11;
then  seq . (n + k) in Y1 ;
hence  ex r1 being real number st
( r1 in Y1 & r - s < r1 ) by A12; ::_thesis: verum
end;
 for r1 being real number st r1 in Y1 holds
r1 <= r
proof
let r1 be real number ; ::_thesis: ( r1 in Y1 implies r1 <= r )
assume  r1 in Y1 ; ::_thesis: r1 <= r
then consider k1 being Element of NAT  such that
A13: r1 = seq . k1 and
A14: n <= k1 ;
consider k2 being Nat such that
A15: k1 = n + k2 by A14, NAT_1:10;
 k2 in NAT by ORDINAL1:def_12;
hence  r1 <= r by A9, A13, A15; ::_thesis: verum
end;
then  r = upper_bound Y1 by A1, A11, SEQ_4:def_1;
hence  r = (superior_realsequence seq) . n by Def5; ::_thesis: verum
end;

theorem Th42: :: RINFSUP1:42
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V89() holds
( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
proof
let n be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence st seq is V89() holds
( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
set seq1 = seq ^\ n;
assume  seq is V89() ; ::_thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n )
then A1: seq ^\ n is V89() by SEQM_3:28;
A2: rng (seq ^\ n) = Y1 by Th30;
thus  ( ( for k being Element of NAT holds r <= seq . (n + k) ) implies r <= (inferior_realsequence seq) . n ) ::_thesis: ( r <= (inferior_realsequence seq) . n implies for k being Element of NAT holds r <= seq . (n + k) )
proof
assume A3: for k being Element of NAT holds r <= seq . (n + k) ; ::_thesis: r <= (inferior_realsequence seq) . n
now__::_thesis:_for_n1_being_Element_of_NAT_holds_r_<=_(seq_^\_n)_._n1
let n1 be Element of NAT ; ::_thesis: r <= (seq ^\ n) . n1
 (seq ^\ n) . n1 in rng (seq ^\ n) by FUNCT_2:4;
then consider r1 being real number  such that
A4: (seq ^\ n) . n1 = r1 and
A5: r1 in Y1 by A2;
consider k1 being Element of NAT  such that
A6: r1 = seq . k1 and
A7: n <= k1 by A5;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
 k2 in NAT by ORDINAL1:def_12;
hence  r <= (seq ^\ n) . n1 by A3, A4, A6, A8; ::_thesis: verum
end;
then  r <= lower_bound (seq ^\ n) by Th10;
then  r <= lower_bound Y1 by Th30;
hence  r <= (inferior_realsequence seq) . n by Def4; ::_thesis: verum
end;
assume  r <= (inferior_realsequence seq) . n ; ::_thesis: for k being Element of NAT holds r <= seq . (n + k)
then  r <= lower_bound Y1 by Def4;
then A9: r <= lower_bound (seq ^\ n) by Th30;
now__::_thesis:_for_m1_being_Element_of_NAT_holds_r_<=_seq_._(n_+_m1)
let m1 be Element of NAT ; ::_thesis: r <= seq . (n + m1)
 n <= n + m1 by NAT_1:11;
then  seq . (n + m1) in Y1 ;
then  seq . (n + m1) in rng (seq ^\ n) by Th30;
then  ex k being set st
( k in dom (seq ^\ n) & (seq ^\ n) . k = seq . (n + m1) ) by FUNCT_1:def_3;
hence  r <= seq . (n + m1) by A1, A9, Th10; ::_thesis: verum
end;
hence  for k being Element of NAT holds r <= seq . (n + k) ; ::_thesis: verum
end;

theorem Th43: :: RINFSUP1:43
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V89() holds
( ( for m being Element of NAT st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
proof
let n be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence st seq is V89() holds
( ( for m being Element of NAT st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
( ( for m being Element of NAT st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( ( for m being Element of NAT st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) )
assume A1: seq is V89() ; ::_thesis: ( ( for m being Element of NAT st n <= m holds
r <= seq . m ) iff r <= (inferior_realsequence seq) . n )
thus  ( ( for m being Element of NAT st n <= m holds
r <= seq . m ) implies r <= (inferior_realsequence seq) . n ) ::_thesis: ( r <= (inferior_realsequence seq) . n implies for m being Element of NAT st n <= m holds
r <= seq . m )
proof
assume  for m being Element of NAT st n <= m holds
r <= seq . m ; ::_thesis: r <= (inferior_realsequence seq) . n
then  for k being Element of NAT holds r <= seq . (n + k) by NAT_1:11;
hence  r <= (inferior_realsequence seq) . n by A1, Th42; ::_thesis: verum
end;
assume A2: r <= (inferior_realsequence seq) . n ; ::_thesis: for m being Element of NAT st n <= m holds
r <= seq . m
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
r_<=_seq_._m
let m be Element of NAT ; ::_thesis: ( n <= m implies r <= seq . m )
assume  n <= m ; ::_thesis: r <= seq . m
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  r <= seq . m by A1, A2, A3, Th42; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
r <= seq . m ; ::_thesis: verum
end;

theorem Th44: :: RINFSUP1:44
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V88() holds
( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )
proof
let n be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence st seq is V88() holds
( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r ) )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
set seq1 = seq ^\ n;
assume  seq is V88() ; ::_thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r )
then A1: seq ^\ n is V88() by SEQM_3:27;
A2: rng (seq ^\ n) = Y1 by Th30;
thus  ( ( for k being Element of NAT holds seq . (n + k) <= r ) implies (superior_realsequence seq) . n <= r ) ::_thesis: ( (superior_realsequence seq) . n <= r implies for k being Element of NAT holds seq . (n + k) <= r )
proof
assume A3: for k being Element of NAT holds seq . (n + k) <= r ; ::_thesis: (superior_realsequence seq) . n <= r
now__::_thesis:_for_n1_being_Element_of_NAT_holds_(seq_^\_n)_._n1_<=_r
let n1 be Element of NAT ; ::_thesis: (seq ^\ n) . n1 <= r
 (seq ^\ n) . n1 in rng (seq ^\ n) by FUNCT_2:4;
then consider r1 being real number  such that
A4: (seq ^\ n) . n1 = r1 and
A5: r1 in Y1 by A2;
consider k1 being Element of NAT  such that
A6: r1 = seq . k1 and
A7: n <= k1 by A5;
consider k2 being Nat such that
A8: k1 = n + k2 by A7, NAT_1:10;
 k2 in NAT by ORDINAL1:def_12;
hence  (seq ^\ n) . n1 <= r by A3, A4, A6, A8; ::_thesis: verum
end;
then  upper_bound (seq ^\ n) <= r by Th9;
then  upper_bound Y1 <= r by Th30;
hence  (superior_realsequence seq) . n <= r by Def5; ::_thesis: verum
end;
assume  (superior_realsequence seq) . n <= r ; ::_thesis: for k being Element of NAT holds seq . (n + k) <= r
then  upper_bound Y1 <= r by Def5;
then A9: upper_bound (seq ^\ n) <= r by Th30;
now__::_thesis:_for_m1_being_Element_of_NAT_holds_seq_._(n_+_m1)_<=_r
let m1 be Element of NAT ; ::_thesis: seq . (n + m1) <= r
 n <= n + m1 by NAT_1:11;
then  seq . (n + m1) in Y1 ;
then  seq . (n + m1) in rng (seq ^\ n) by Th30;
then  ex k being set st
( k in dom (seq ^\ n) & (seq ^\ n) . k = seq . (n + m1) ) by FUNCT_1:def_3;
hence  seq . (n + m1) <= r by A1, A9, Th9; ::_thesis: verum
end;
hence  for k being Element of NAT holds seq . (n + k) <= r ; ::_thesis: verum
end;

theorem Th45: :: RINFSUP1:45
for n being Element of NAT
for r being real number
for seq being Real_Sequence st seq is V88() holds
( ( for m being Element of NAT st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
proof
let n be Element of NAT ; ::_thesis: for r being real number
for seq being Real_Sequence st seq is V88() holds
( ( for m being Element of NAT st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
( ( for m being Element of NAT st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( ( for m being Element of NAT st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r ) )
assume A1: seq is V88() ; ::_thesis: ( ( for m being Element of NAT st n <= m holds
seq . m <= r ) iff (superior_realsequence seq) . n <= r )
thus  ( ( for m being Element of NAT st n <= m holds
seq . m <= r ) implies (superior_realsequence seq) . n <= r ) ::_thesis: ( (superior_realsequence seq) . n <= r implies for m being Element of NAT st n <= m holds
seq . m <= r )
proof
assume  for m being Element of NAT st n <= m holds
seq . m <= r ; ::_thesis: (superior_realsequence seq) . n <= r
then  for k being Element of NAT holds seq . (n + k) <= r by NAT_1:11;
hence  (superior_realsequence seq) . n <= r by A1, Th44; ::_thesis: verum
end;
assume A2: (superior_realsequence seq) . n <= r ; ::_thesis: for m being Element of NAT st n <= m holds
seq . m <= r
now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_
seq_._m_<=_r
let m be Element of NAT ; ::_thesis: ( n <= m implies seq . m <= r )
assume  n <= m ; ::_thesis: seq . m <= r
then consider k being Nat such that
A3: m = n + k by NAT_1:10;
 k in NAT by ORDINAL1:def_12;
hence  seq . m <= r by A1, A2, A3, Th44; ::_thesis: verum
end;
hence  for m being Element of NAT st n <= m holds
seq . m <= r ; ::_thesis: verum
end;

theorem Th46: :: RINFSUP1:46
for n being Element of NAT
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) )
reconsider Y2 =  {  (seq . k) where k is Element of NAT : n + 1 <= k  }  as Subset of REAL by Th29;
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
reconsider Y3 = {(seq . n)} as Subset of REAL ;
A1: (inferior_realsequence seq) . (n + 1) = lower_bound Y2 by Def4;
assume A2: seq is V89() ; ::_thesis: (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n))
then A3: ( Y2 <> {} & Y2 is bounded_below ) by Th32, SETLIM_1:1;
A4: Y3 is bounded_below
proof
consider t being real number  such that
A5: for m being Element of NAT holds t < seq . m by A2, SEQ_2:def_4;
 t is LowerBound of Y3
proof
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Y3 or t <= r )
assume  r in Y3 ; ::_thesis: t <= r
then  r = seq . n by TARSKI:def_1;
hence  t <= r by A5; ::_thesis: verum
end;
hence  Y3 is bounded_below by XXREAL_2:def_9; ::_thesis: verum
end;
 (inferior_realsequence seq) . n = lower_bound Y1 by Def4;
then (inferior_realsequence seq) . n = lower_bound (Y2 \/ Y3) by SETLIM_1:2
.= min ((lower_bound Y2),(lower_bound Y3)) by A3, A4, SEQ_4:142
.= min (((inferior_realsequence seq) . (n + 1)),(seq . n)) by A1, SEQ_4:9 ;
hence  (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) ; ::_thesis: verum
end;

theorem Th47: :: RINFSUP1:47
for n being Element of NAT
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) )
reconsider Y2 =  {  (seq . k) where k is Element of NAT : n + 1 <= k  }  as Subset of REAL by Th29;
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
reconsider Y3 = {(seq . n)} as Subset of REAL ;
A1: (superior_realsequence seq) . (n + 1) = upper_bound Y2 by Def5;
assume A2: seq is V88() ; ::_thesis: (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n))
then A3: ( Y2 <> {} & Y2 is bounded_above ) by Th31, SETLIM_1:1;
A4: Y3 is bounded_above
proof
consider t being real number  such that
A5: for m being Element of NAT holds seq . m < t by A2, SEQ_2:def_3;
 t is UpperBound of Y3
proof
let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in Y3 or r <= t )
assume  r in Y3 ; ::_thesis: r <= t
then  r = seq . n by TARSKI:def_1;
hence  r <= t by A5; ::_thesis: verum
end;
hence  Y3 is bounded_above by XXREAL_2:def_10; ::_thesis: verum
end;
 (superior_realsequence seq) . n = upper_bound Y1 by Def5;
then (superior_realsequence seq) . n = upper_bound (Y2 \/ Y3) by SETLIM_1:2
.= max ((upper_bound Y2),(upper_bound Y3)) by A3, A4, SEQ_4:143
.= max (((superior_realsequence seq) . (n + 1)),(seq . n)) by A1, SEQ_4:9 ;
hence  (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) ; ::_thesis: verum
end;

theorem Th48: :: RINFSUP1:48
for n being Element of NAT
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) )
A1: min (((inferior_realsequence seq) . (n + 1)),(seq . n)) <= (inferior_realsequence seq) . (n + 1) by XXREAL_0:17;
assume  seq is V89() ; ::_thesis: (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1)
hence  (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by A1, Th46; ::_thesis: verum
end;

theorem Th49: :: RINFSUP1:49
for n being Element of NAT
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n )
A1: (superior_realsequence seq) . (n + 1) <= max (((superior_realsequence seq) . (n + 1)),(seq . n)) by XXREAL_0:25;
assume  seq is V88() ; ::_thesis: (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n
hence  (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n by A1, Th47; ::_thesis: verum
end;

theorem Th50: :: RINFSUP1:50
for seq being Real_Sequence st seq is V89() holds
inferior_realsequence seq is V48()
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies inferior_realsequence seq is V48() )
assume  seq is V89() ; ::_thesis: inferior_realsequence seq is V48()
then  for n being Element of NAT holds (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by Th48;
hence  inferior_realsequence seq is V48() by SEQM_3:def_8; ::_thesis: verum
end;

theorem Th51: :: RINFSUP1:51
for seq being Real_Sequence st seq is V88() holds
superior_realsequence seq is V49()
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies superior_realsequence seq is V49() )
assume  seq is V88() ; ::_thesis: superior_realsequence seq is V49()
then  for n being Element of NAT holds (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n by Th49;
hence  superior_realsequence seq is V49() by SEQM_3:def_9; ::_thesis: verum
end;

theorem :: RINFSUP1:52
for n being Element of NAT
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= (superior_realsequence seq) . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= (superior_realsequence seq) . n
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies (inferior_realsequence seq) . n <= (superior_realsequence seq) . n )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
assume A1: seq is bounded ; ::_thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n
A2: Y1 <> {} by SETLIM_1:1;
 ( (superior_realsequence seq) . n = upper_bound Y1 & (inferior_realsequence seq) . n = lower_bound Y1 ) by Def4, Def5;
hence  (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A1, A2, Th33, SEQ_4:11; ::_thesis: verum
end;

theorem Th53: :: RINFSUP1:53
for n being Element of NAT
for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
(inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq)
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) )
reconsider Y2 =  {  (seq . k2) where k2 is Element of NAT : n <= k2  }  as Subset of REAL by Th29;
assume A1: seq is bounded ; ::_thesis: (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq)
A2: now__::_thesis:_for_m_being_Element_of_NAT_holds_lower_bound_Y2_<=_(superior_realsequence_seq)_._m
let m be Element of NAT ; ::_thesis: lower_bound Y2 <= (superior_realsequence seq) . m
reconsider Y1 =  {  (seq . k1) where k1 is Element of NAT : m <= k1  }  as Subset of REAL by Th29;
 n <= n + m by NAT_1:11;
then A3: seq . (n + m) in Y2 ;
 Y2 is real-bounded by A1, Th33;
then  Y2 is bounded_below by XXREAL_2:def_11;
then A4: lower_bound Y2 <= seq . (n + m) by A3, SEQ_4:def_2;
 m <= n + m by NAT_1:11;
then A5: seq . (n + m) in Y1 ;
 Y1 is real-bounded by A1, Th33;
then  Y1 is bounded_above by XXREAL_2:def_11;
then A6: seq . (n + m) <= upper_bound Y1 by A5, SEQ_4:def_1;
 (superior_realsequence seq) . m = upper_bound Y1 by Def5;
hence  lower_bound Y2 <= (superior_realsequence seq) . m by A6, A4, XXREAL_0:2; ::_thesis: verum
end;
 (inferior_realsequence seq) . n = lower_bound Y2 by Def4;
hence  (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) by A2, Th10; ::_thesis: verum
end;

theorem Th54: :: RINFSUP1:54
for n being Element of NAT
for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n )
reconsider Y2 =  {  (seq . k2) where k2 is Element of NAT : n <= k2  }  as Subset of REAL by Th29;
assume A1: seq is bounded ; ::_thesis: upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n
A2: now__::_thesis:_for_m_being_Element_of_NAT_holds_upper_bound_Y2_>=_(inferior_realsequence_seq)_._m
let m be Element of NAT ; ::_thesis: upper_bound Y2 >= (inferior_realsequence seq) . m
reconsider Y1 =  {  (seq . k1) where k1 is Element of NAT : m <= k1  }  as Subset of REAL by Th29;
 n <= n + m by NAT_1:11;
then A3: seq . (n + m) in Y2 ;
 Y2 is real-bounded by A1, Th33;
then  Y2 is bounded_above by XXREAL_2:def_11;
then A4: upper_bound Y2 >= seq . (n + m) by A3, SEQ_4:def_1;
 m <= n + m by NAT_1:11;
then A5: seq . (n + m) in Y1 ;
 Y1 is real-bounded by A1, Th33;
then  Y1 is bounded_below by XXREAL_2:def_11;
then A6: seq . (n + m) >= lower_bound Y1 by A5, SEQ_4:def_2;
 (inferior_realsequence seq) . m = lower_bound Y1 by Def4;
hence  upper_bound Y2 >= (inferior_realsequence seq) . m by A6, A4, XXREAL_0:2; ::_thesis: verum
end;
 (superior_realsequence seq) . n = upper_bound Y2 by Def5;
hence  upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n by A2, Th9; ::_thesis: verum
end;

theorem Th55: :: RINFSUP1:55
for seq being Real_Sequence st seq is bounded holds
upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) )
set seq1 = inferior_realsequence seq;
set r = lower_bound (superior_realsequence seq);
assume  seq is bounded ; ::_thesis: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq)
then  for n being Element of NAT holds (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) by Th53;
hence  upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by Th9; ::_thesis: verum
end;

theorem Th56: :: RINFSUP1:56
for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) )
assume A1: seq is bounded ; ::_thesis: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded )
then  inferior_realsequence seq is V48() by Th50;
then A2: inferior_realsequence seq is V89() by LIMFUNC1:1;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(upper_bound_(inferior_realsequence_seq))_-_1_<_(superior_realsequence_seq)_._m
let m be Element of NAT ; ::_thesis: (upper_bound (inferior_realsequence seq)) - 1 < (superior_realsequence seq) . m
 upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . m by A1, Th54;
hence  (upper_bound (inferior_realsequence seq)) - 1 < (superior_realsequence seq) . m by Lm1; ::_thesis: verum
end;
then A3: superior_realsequence seq is V89() by SEQ_2:def_4;
now__::_thesis:_for_m_being_Element_of_NAT_holds_(inferior_realsequence_seq)_._m_<_(lower_bound_(superior_realsequence_seq))_+_1
let m be Element of NAT ; ::_thesis: (inferior_realsequence seq) . m < (lower_bound (superior_realsequence seq)) + 1
 (inferior_realsequence seq) . m <= lower_bound (superior_realsequence seq) by A1, Th53;
hence  (inferior_realsequence seq) . m < (lower_bound (superior_realsequence seq)) + 1 by Lm1; ::_thesis: verum
end;
then A4: inferior_realsequence seq is V88() by SEQ_2:def_3;
 superior_realsequence seq is V49() by A1, Th51;
then  superior_realsequence seq is V88() by LIMFUNC1:1;
hence  ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A2, A4, A3; ::_thesis: verum
end;

theorem Th57: :: RINFSUP1:57
for seq being Real_Sequence st seq is bounded holds
( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) )
assume  seq is bounded ; ::_thesis: ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) )
then  ( inferior_realsequence seq is V48() & inferior_realsequence seq is bounded ) by Th50, Th56;
hence  ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) by Th24; ::_thesis: verum
end;

theorem Th58: :: RINFSUP1:58
for seq being Real_Sequence st seq is bounded holds
( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) )
assume  seq is bounded ; ::_thesis: ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) )
then  ( superior_realsequence seq is V49() & superior_realsequence seq is bounded ) by Th51, Th56;
hence  ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) by Th25; ::_thesis: verum
end;

theorem Th59: :: RINFSUP1:59
for n being Element of NAT
for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V89() holds
(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) )
assume A1: seq is V89() ; ::_thesis: (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)
(inferior_realsequence seq) . n = lower_bound (seq ^\ n) by Th36
.= - (upper_bound (- (seq ^\ n))) by A1, Th14, SEQM_3:28
.= - (upper_bound ((- seq) ^\ n)) by SEQM_3:16 ;
hence  (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th37; ::_thesis: verum
end;

theorem Th60: :: RINFSUP1:60
for n being Element of NAT
for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V88() holds
(superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) )
assume A1: seq is V88() ; ::_thesis: (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n)
(superior_realsequence seq) . n = upper_bound (seq ^\ n) by Th37
.= - (lower_bound (- (seq ^\ n))) by A1, Th13, SEQM_3:27
.= - (lower_bound ((- seq) ^\ n)) by SEQM_3:16 ;
hence  (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) by Th36; ::_thesis: verum
end;

theorem Th61: :: RINFSUP1:61
for seq being Real_Sequence st seq is V89() holds
inferior_realsequence seq = - (superior_realsequence (- seq))
proof
let seq be Real_Sequence; ::_thesis: ( seq is V89() implies inferior_realsequence seq = - (superior_realsequence (- seq)) )
assume  seq is V89() ; ::_thesis: inferior_realsequence seq = - (superior_realsequence (- seq))
then  for n being Element of NAT holds (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th59;
hence  inferior_realsequence seq = - (superior_realsequence (- seq)) by SEQ_1:10; ::_thesis: verum
end;

theorem Th62: :: RINFSUP1:62
for seq being Real_Sequence st seq is V88() holds
superior_realsequence seq = - (inferior_realsequence (- seq))
proof
let seq be Real_Sequence; ::_thesis: ( seq is V88() implies superior_realsequence seq = - (inferior_realsequence (- seq)) )
assume  seq is V88() ; ::_thesis: superior_realsequence seq = - (inferior_realsequence (- seq))
then  for n being Element of NAT holds (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) by Th60;
hence  superior_realsequence seq = - (inferior_realsequence (- seq)) by SEQ_1:10; ::_thesis: verum
end;

theorem :: RINFSUP1:63
for n being Element of NAT
for seq being Real_Sequence st seq is V48() holds
seq . n <= (inferior_realsequence seq) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() holds
seq . n <= (inferior_realsequence seq) . (n + 1)
let seq be Real_Sequence; ::_thesis: ( seq is V48() implies seq . n <= (inferior_realsequence seq) . (n + 1) )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n + 1 <= k  }  as Subset of REAL by Th29;
A1: (inferior_realsequence seq) . (n + 1) = lower_bound Y1 by Def4;
assume A2: seq is V48() ; ::_thesis: seq . n <= (inferior_realsequence seq) . (n + 1)
then  lower_bound Y1 = seq . (n + 1) by Th34;
hence  seq . n <= (inferior_realsequence seq) . (n + 1) by A2, A1, SEQM_3:def_8; ::_thesis: verum
end;

Lm2:  for n being Element of NAT
for seq being Real_Sequence st seq is V48() holds
(inferior_realsequence seq) . n = seq . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() holds
(inferior_realsequence seq) . n = seq . n
let seq be Real_Sequence; ::_thesis: ( seq is V48() implies (inferior_realsequence seq) . n = seq . n )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
assume A1: seq is V48() ; ::_thesis: (inferior_realsequence seq) . n = seq . n
 (inferior_realsequence seq) . n = lower_bound Y1 by Def4;
hence  (inferior_realsequence seq) . n = seq . n by A1, Th34; ::_thesis: verum
end;

theorem :: RINFSUP1:64
for seq being Real_Sequence st seq is V48() holds
inferior_realsequence seq = seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V48() implies inferior_realsequence seq = seq )
assume  seq is V48() ; ::_thesis: inferior_realsequence seq = seq
then  for n being Element of NAT holds (inferior_realsequence seq) . n = seq . n by Lm2;
hence  inferior_realsequence seq = seq by FUNCT_2:63; ::_thesis: verum
end;

theorem Th65: :: RINFSUP1:65
for n being Element of NAT
for seq being Real_Sequence st seq is V48() & seq is V88() holds
seq . n <= (superior_realsequence seq) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() & seq is V88() holds
seq . n <= (superior_realsequence seq) . (n + 1)
let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies seq . n <= (superior_realsequence seq) . (n + 1) )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n + 1 <= k  }  as Subset of REAL by Th29;
A1: seq . (n + 1) in Y1 ;
assume A2: ( seq is V48() & seq is V88() ) ; ::_thesis: seq . n <= (superior_realsequence seq) . (n + 1)
then  Y1 is bounded_above by Th31;
then A3: seq . (n + 1) <= upper_bound Y1 by A1, SEQ_4:def_1;
A4: (superior_realsequence seq) . (n + 1) = upper_bound Y1 by Def5;
 seq . n <= seq . (n + 1) by A2, SEQM_3:def_8;
hence  seq . n <= (superior_realsequence seq) . (n + 1) by A4, A3, XXREAL_0:2; ::_thesis: verum
end;

theorem Th66: :: RINFSUP1:66
for n being Element of NAT
for seq being Real_Sequence st seq is V48() & seq is V88() holds
(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() & seq is V88() holds
(superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)
let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) )
assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1)
then  seq . n <= (superior_realsequence seq) . (n + 1) by Th65;
then  max (((superior_realsequence seq) . (n + 1)),(seq . n)) = (superior_realsequence seq) . (n + 1) by XXREAL_0:def_10;
hence  (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) by A1, Th47; ::_thesis: verum
end;

theorem Th67: :: RINFSUP1:67
for n being Element of NAT
for seq being Real_Sequence st seq is V48() & seq is V88() holds
( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() & seq is V88() holds
( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )
let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) )
defpred S1[ Nat] means (superior_realsequence seq) . $1 = upper_bound seq;
assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant )
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
 k in NAT by ORDINAL1:def_12;
hence  ( S1[k] implies S1[k + 1] ) by A1, Th66; ::_thesis: verum
end;
A3: S1[ 0 ] by A1, Th39;
 for k being Nat holds S1[k] from NAT_1:sch_2(A3, A2);
hence  ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) by VALUED_0:def_18; ::_thesis: verum
end;

theorem :: RINFSUP1:68
for seq being Real_Sequence st seq is V48() & seq is V88() holds
lower_bound (superior_realsequence seq) = upper_bound seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies lower_bound (superior_realsequence seq) = upper_bound seq )
assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: lower_bound (superior_realsequence seq) = upper_bound seq
then  superior_realsequence seq is constant by Th67;
then consider r1 being Real such that
A2: rng (superior_realsequence seq) = {r1} by FUNCT_2:111;
 r1 in rng (superior_realsequence seq) by A2, TARSKI:def_1;
then  ex n being Element of NAT st r1 = (superior_realsequence seq) . n by FUNCT_2:113;
then  rng (superior_realsequence seq) = {(upper_bound seq)} by A1, A2, Th67;
hence  lower_bound (superior_realsequence seq) = upper_bound seq by SEQ_4:9; ::_thesis: verum
end;

theorem :: RINFSUP1:69
for n being Element of NAT
for seq being Real_Sequence st seq is V49() holds
(superior_realsequence seq) . (n + 1) <= seq . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() holds
(superior_realsequence seq) . (n + 1) <= seq . n
let seq be Real_Sequence; ::_thesis: ( seq is V49() implies (superior_realsequence seq) . (n + 1) <= seq . n )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n + 1 <= k  }  as Subset of REAL by Th29;
A1: (superior_realsequence seq) . (n + 1) = upper_bound Y1 by Def5;
assume A2: seq is V49() ; ::_thesis: (superior_realsequence seq) . (n + 1) <= seq . n
then  upper_bound Y1 = seq . (n + 1) by Th35;
hence  (superior_realsequence seq) . (n + 1) <= seq . n by A2, A1, SEQM_3:def_9; ::_thesis: verum
end;

Lm3:  for n being Element of NAT
for seq being Real_Sequence st seq is V49() holds
(superior_realsequence seq) . n = seq . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() holds
(superior_realsequence seq) . n = seq . n
let seq be Real_Sequence; ::_thesis: ( seq is V49() implies (superior_realsequence seq) . n = seq . n )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n <= k  }  as Subset of REAL by Th29;
assume A1: seq is V49() ; ::_thesis: (superior_realsequence seq) . n = seq . n
 (superior_realsequence seq) . n = upper_bound Y1 by Def5;
hence  (superior_realsequence seq) . n = seq . n by A1, Th35; ::_thesis: verum
end;

theorem :: RINFSUP1:70
for seq being Real_Sequence st seq is V49() holds
superior_realsequence seq = seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V49() implies superior_realsequence seq = seq )
assume  seq is V49() ; ::_thesis: superior_realsequence seq = seq
then  for n being Element of NAT holds (superior_realsequence seq) . n = seq . n by Lm3;
hence  superior_realsequence seq = seq by FUNCT_2:63; ::_thesis: verum
end;

theorem Th71: :: RINFSUP1:71
for n being Element of NAT
for seq being Real_Sequence st seq is V49() & seq is V89() holds
(inferior_realsequence seq) . (n + 1) <= seq . n
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds
(inferior_realsequence seq) . (n + 1) <= seq . n
let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies (inferior_realsequence seq) . (n + 1) <= seq . n )
reconsider Y1 =  {  (seq . k) where k is Element of NAT : n + 1 <= k  }  as Subset of REAL by Th29;
A1: seq . (n + 1) in Y1 ;
assume A2: ( seq is V49() & seq is V89() ) ; ::_thesis: (inferior_realsequence seq) . (n + 1) <= seq . n
then  Y1 is bounded_below by Th32;
then A3: lower_bound Y1 <= seq . (n + 1) by A1, SEQ_4:def_2;
A4: (inferior_realsequence seq) . (n + 1) = lower_bound Y1 by Def4;
 seq . (n + 1) <= seq . n by A2, SEQM_3:def_9;
hence  (inferior_realsequence seq) . (n + 1) <= seq . n by A4, A3, XXREAL_0:2; ::_thesis: verum
end;

theorem Th72: :: RINFSUP1:72
for n being Element of NAT
for seq being Real_Sequence st seq is V49() & seq is V89() holds
(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds
(inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)
let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) )
assume A1: ( seq is V49() & seq is V89() ) ; ::_thesis: (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1)
then  (inferior_realsequence seq) . (n + 1) <= seq . n by Th71;
then  min (((inferior_realsequence seq) . (n + 1)),(seq . n)) = (inferior_realsequence seq) . (n + 1) by XXREAL_0:def_9;
hence  (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) by A1, Th46; ::_thesis: verum
end;

theorem Th73: :: RINFSUP1:73
for n being Element of NAT
for seq being Real_Sequence st seq is V49() & seq is V89() holds
( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )
proof
let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds
( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )
let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) )
assume that
A1: seq is V49() and
A2: seq is V89() ; ::_thesis: ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant )
defpred S1[ Nat] means (inferior_realsequence seq) . $1 = lower_bound seq;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
 k in NAT by ORDINAL1:def_12;
hence  ( S1[k] implies S1[k + 1] ) by A1, A2, Th72; ::_thesis: verum
end;
A4: S1[ 0 ] by A2, Th38;
 for k being Nat holds S1[k] from NAT_1:sch_2(A4, A3);
hence  ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) by VALUED_0:def_18; ::_thesis: verum
end;

theorem :: RINFSUP1:74
for seq being Real_Sequence st seq is V49() & seq is V89() holds
upper_bound (inferior_realsequence seq) = lower_bound seq
proof
let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies upper_bound (inferior_realsequence seq) = lower_bound seq )
assume A1: ( seq is V49() & seq is V89() ) ; ::_thesis: upper_bound (inferior_realsequence seq) = lower_bound seq
then  inferior_realsequence seq is constant by Th73;
then consider r1 being Real such that
A2: rng (inferior_realsequence seq) = {r1} by FUNCT_2:111;
 r1 in rng (inferior_realsequence seq) by A2, TARSKI:def_1;
then  ex n being Element of NAT st r1 = (inferior_realsequence seq) . n by FUNCT_2:113;
then  upper_bound (inferior_realsequence seq) = upper_bound {(lower_bound seq)} by A1, A2, Th73
.= lower_bound seq by SEQ_4:9 ;
hence  upper_bound (inferior_realsequence seq) = lower_bound seq ; ::_thesis: verum
end;

theorem Th75: :: RINFSUP1:75
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; ::_thesis: ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_
(_(superior_realsequence_seq1)_._n_<=_(superior_realsequence_seq2)_._n_&_(inferior_realsequence_seq1)_._n_<=_(inferior_realsequence_seq2)_._n_)
let n be Element of NAT ; ::_thesis: ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n )
reconsider Y2 =  {  (seq2 . k2) where k2 is Element of NAT : n <= k2  }  as Subset of REAL by Th29;
reconsider Y1 =  {  (seq1 . k1) where k1 is Element of NAT : n <= k1  }  as Subset of REAL by Th29;
A4: ( Y1 <> {} & Y2 <> {} ) by SETLIM_1:1;
A5: ( (inferior_realsequence seq1) . n = lower_bound Y1 & (inferior_realsequence seq2) . n = lower_bound Y2 ) by Def4;
 Y1 is real-bounded by A1, Th33;
then A6: Y1 is bounded_below by XXREAL_2:def_11;
now__::_thesis:_for_r_being_real_number_st_r_in_Y2_holds_
lower_bound_Y1_<=_r
let r be real number ; ::_thesis: ( r in Y2 implies lower_bound Y1 <= r )
assume  r in Y2 ; ::_thesis: lower_bound Y1 <= r
then consider k being Element of NAT  such that
A7: r = seq2 . k and
A8: n <= k ;
 seq1 . k in Y1 by A8;
then A9: lower_bound Y1 <= seq1 . k by A6, SEQ_4:def_2;
 seq1 . k <= r by A3, A7;
hence  lower_bound Y1 <= r by A9, XXREAL_0:2; ::_thesis: verum
end;
then A10: for r being Real st r in Y2 holds
lower_bound Y1 <= r ;
 Y2 is real-bounded by A2, Th33;
then A11: Y2 is bounded_above by XXREAL_2:def_11;
A12: now__::_thesis:_for_r_being_real_number_st_r_in_Y1_holds_
r_<=_upper_bound_Y2
let r be real number ; ::_thesis: ( r in Y1 implies r <= upper_bound Y2 )
assume  r in Y1 ; ::_thesis: r <= upper_bound Y2
then consider k being Element of NAT  such that
A13: r = seq1 . k and
A14: n <= k ;
 seq2 . k in Y2 by A14;
then A15: seq2 . k <= upper_bound Y2 by A11, SEQ_4:def_1;
 r <= seq2 . k by A3, A13;
hence  r <= upper_bound Y2 by A15, XXREAL_0:2; ::_thesis: verum
end;
 ( (superior_realsequence seq1) . n = upper_bound Y1 & (superior_realsequence seq2) . n = upper_bound Y2 ) by Def5;
hence  ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) by A5, A4, A12, A10, SEQ_4:113, SEQ_4:144; ::_thesis: verum
end;
hence  ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) ; ::_thesis: verum
end;

theorem :: RINFSUP1:76
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds
(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)
proof
let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds
(inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq2 is V89() implies (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) )
assume  ( seq1 is V89() & seq2 is V89() ) ; ::_thesis: (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n)
then  ( seq1 ^\ n is V89() & seq2 ^\ n is V89() ) by SEQM_3:28;
then  lower_bound ((seq1 ^\ n) + (seq2 ^\ n)) >= (lower_bound (seq1 ^\ n)) + (lower_bound (seq2 ^\ n)) by Th15;
then A1: lower_bound ((seq1 + seq2) ^\ n) >= (lower_bound (seq1 ^\ n)) + (lower_bound (seq2 ^\ n)) by SEQM_3:15;
 ( (inferior_realsequence seq1) . n = lower_bound (seq1 ^\ n) & (inferior_realsequence seq2) . n = lower_bound (seq2 ^\ n) ) by Th36;
hence  (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) by A1, Th36; ::_thesis: verum
end;

theorem :: RINFSUP1:77
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds
(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)
proof
let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds
(superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq2 is V88() implies (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) )
assume  ( seq1 is V88() & seq2 is V88() ) ; ::_thesis: (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n)
then  ( seq1 ^\ n is V88() & seq2 ^\ n is V88() ) by SEQM_3:27;
then  upper_bound ((seq1 ^\ n) + (seq2 ^\ n)) <= (upper_bound (seq1 ^\ n)) + (upper_bound (seq2 ^\ n)) by Th16;
then A1: upper_bound ((seq1 + seq2) ^\ n) <= (upper_bound (seq1 ^\ n)) + (upper_bound (seq2 ^\ n)) by SEQM_3:15;
 ( (superior_realsequence seq1) . n = upper_bound (seq1 ^\ n) & (superior_realsequence seq2) . n = upper_bound (seq2 ^\ n) ) by Th37;
hence  (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) by A1, Th37; ::_thesis: verum
end;

theorem :: RINFSUP1:78
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
proof
let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative implies (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) )
assume  ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative ) ; ::_thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
then  ( seq1 ^\ n is V89() & seq1 ^\ n is nonnegative & seq2 ^\ n is V89() & seq2 ^\ n is nonnegative ) by Th17, SEQM_3:28;
then  lower_bound ((seq1 ^\ n) (#) (seq2 ^\ n)) >= (lower_bound (seq1 ^\ n)) * (lower_bound (seq2 ^\ n)) by Th20;
then A1: lower_bound ((seq1 (#) seq2) ^\ n) >= (lower_bound (seq1 ^\ n)) * (lower_bound (seq2 ^\ n)) by SEQM_3:19;
 ( (inferior_realsequence seq1) . n = lower_bound (seq1 ^\ n) & (inferior_realsequence seq2) . n = lower_bound (seq2 ^\ n) ) by Th36;
hence  (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A1, Th36; ::_thesis: verum
end;

theorem Th79: :: RINFSUP1:79
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
proof
let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds
(inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative implies (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) )
assume  ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative ) ; ::_thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n)
then  ( seq1 ^\ n is V89() & seq1 ^\ n is nonnegative & seq2 ^\ n is V89() & seq2 ^\ n is nonnegative ) by Th17, SEQM_3:28;
then  lower_bound ((seq1 ^\ n) (#) (seq2 ^\ n)) >= (lower_bound (seq1 ^\ n)) * (lower_bound (seq2 ^\ n)) by Th20;
then A1: lower_bound ((seq1 (#) seq2) ^\ n) >= (lower_bound (seq1 ^\ n)) * (lower_bound (seq2 ^\ n)) by SEQM_3:19;
 ( (inferior_realsequence seq1) . n = lower_bound (seq1 ^\ n) & (inferior_realsequence seq2) . n = lower_bound (seq2 ^\ n) ) by Th36;
hence  (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A1, Th36; ::_thesis: verum
end;

theorem Th80: :: RINFSUP1:80
for n being Element of NAT
for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)
proof
let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds
(superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative implies (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) )
assume  ( seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative ) ; ::_thesis: (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n)
then  ( seq1 ^\ n is V88() & seq1 ^\ n is nonnegative & seq2 ^\ n is V88() & seq2 ^\ n is nonnegative ) by Th17, SEQM_3:27;
then  upper_bound ((seq1 ^\ n) (#) (seq2 ^\ n)) <= (upper_bound (seq1 ^\ n)) * (upper_bound (seq2 ^\ n)) by Th21;
then A1: upper_bound ((seq1 (#) seq2) ^\ n) <= (upper_bound (seq1 ^\ n)) * (upper_bound (seq2 ^\ n)) by SEQM_3:19;
 ( (superior_realsequence seq1) . n = upper_bound (seq1 ^\ n) & (superior_realsequence seq2) . n = upper_bound (seq2 ^\ n) ) by Th37;
hence  (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) by A1, Th37; ::_thesis: verum
end;

definition
let seq be Real_Sequence;
func lim_sup seq ->  Element of REAL  equals :: RINFSUP1:def 6
 lower_bound (superior_realsequence seq);
coherence
 lower_bound (superior_realsequence seq) is Element of REAL ;
end;

:: deftheorem  defines lim_sup RINFSUP1:def_6_:_
 for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq);

definition
let seq be Real_Sequence;
func lim_inf seq ->  Element of REAL  equals :: RINFSUP1:def 7
 upper_bound (inferior_realsequence seq);
coherence
 upper_bound (inferior_realsequence seq) is Element of REAL ;
end;

:: deftheorem  defines lim_inf RINFSUP1:def_7_:_
 for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq);

theorem Th81: :: RINFSUP1:81
for r being real number
for seq being Real_Sequence st seq is bounded holds
( lim_inf seq <= r iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
( lim_inf seq <= r iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s )
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( lim_inf seq <= r iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) )
set seq1 = inferior_realsequence seq;
assume A1: seq is bounded ; ::_thesis: ( lim_inf seq <= r iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s )
then A2: inferior_realsequence seq is bounded by Th56;
thus  ( lim_inf seq <= r implies for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) ::_thesis: ( ( for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) implies lim_inf seq <= r )
proof
assume A3: lim_inf seq <= r ; ::_thesis: for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s
let s be real number ; ::_thesis: ( 0 < s implies for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s )
assume A4: 0 < s ; ::_thesis: for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s
 for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st seq . (n + k) < r + s
consider k being Element of NAT  such that
A5: seq . (n + k) < ((inferior_realsequence seq) . n) + s by A1, A4, Th40;
 (inferior_realsequence seq) . n <= r by A2, A3, Th9;
then  (seq . (n + k)) + ((inferior_realsequence seq) . n) < r + (((inferior_realsequence seq) . n) + s) by A5, XREAL_1:8;
then  seq . (n + k) < (r + (((inferior_realsequence seq) . n) + s)) - ((inferior_realsequence seq) . n) by XREAL_1:20;
hence  ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: verum
end;
hence  for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: verum
end;
assume A6: for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: lim_inf seq <= r
 for s being real number st 0 < s holds
lim_inf seq <= r + s
proof
let s be real number ; ::_thesis: ( 0 < s implies lim_inf seq <= r + s )
assume A7: 0 < s ; ::_thesis: lim_inf seq <= r + s
 for n being Element of NAT holds (inferior_realsequence seq) . n <= r + s
proof
let n be Element of NAT ; ::_thesis: (inferior_realsequence seq) . n <= r + s
consider k being Element of NAT  such that
A8: seq . (n + k) < r + s by A6, A7;
 (inferior_realsequence seq) . n <= seq . (n + k) by A1, Th40;
hence  (inferior_realsequence seq) . n <= r + s by A8, XXREAL_0:2; ::_thesis: verum
end;
hence  lim_inf seq <= r + s by Th9; ::_thesis: verum
end;
hence  lim_inf seq <= r by XREAL_1:41; ::_thesis: verum
end;

theorem Th82: :: RINFSUP1:82
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) )
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
set seq1 = inferior_realsequence seq;
assume A1: seq is bounded ; ::_thesis: ( r <= lim_inf seq iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) )
then A2: inferior_realsequence seq is bounded by Th56;
thus  ( r <= lim_inf seq implies for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ::_thesis: ( ( for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) implies r <= lim_inf seq )
proof
assume A3: r <= lim_inf seq ; ::_thesis: for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k)
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) )
assume A4: 0 < s ; ::_thesis: ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k)
 ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k)
proof
consider n1 being Element of NAT  such that
A5: (inferior_realsequence seq) . n1 > (upper_bound (inferior_realsequence seq)) - s by A2, A4, Th7;
 ((inferior_realsequence seq) . n1) + (upper_bound (inferior_realsequence seq)) > r + ((upper_bound (inferior_realsequence seq)) - s) by A3, A5, XREAL_1:8;
then  ((inferior_realsequence seq) . n1) + (upper_bound (inferior_realsequence seq)) > (r - s) + (upper_bound (inferior_realsequence seq)) ;
then A6: (((inferior_realsequence seq) . n1) + (upper_bound (inferior_realsequence seq))) - (upper_bound (inferior_realsequence seq)) > r - s by XREAL_1:20;
now__::_thesis:_for_k_being_Element_of_NAT_holds_r_-_s_<_seq_._(n1_+_k)
let k be Element of NAT ; ::_thesis: r - s < seq . (n1 + k)
 (inferior_realsequence seq) . n1 <= seq . (n1 + k) by A1, Th40;
then  (r - s) + ((inferior_realsequence seq) . n1) < (seq . (n1 + k)) + ((inferior_realsequence seq) . n1) by A6, XREAL_1:8;
then  ((r - s) + ((inferior_realsequence seq) . n1)) - ((inferior_realsequence seq) . n1) < seq . (n1 + k) by XREAL_1:19;
hence  r - s < seq . (n1 + k) ; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ; ::_thesis: verum
end;
assume A7: for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ; ::_thesis: r <= lim_inf seq
 for s being real number st 0 < s holds
r - s <= lim_inf seq
proof
let s be real number ; ::_thesis: ( 0 < s implies r - s <= lim_inf seq )
assume  0 < s ; ::_thesis: r - s <= lim_inf seq
then consider n1 being Element of NAT  such that
A8: for k being Element of NAT holds r - s < seq . (n1 + k) by A7;
 for k being Element of NAT holds r - s <= seq . (n1 + k) by A8;
then A9: r - s <= (inferior_realsequence seq) . n1 by A1, Th42;
 (inferior_realsequence seq) . n1 <= upper_bound (inferior_realsequence seq) by A2, Th7;
hence  r - s <= lim_inf seq by A9, XXREAL_0:2; ::_thesis: verum
end;
hence  r <= lim_inf seq by XREAL_1:57; ::_thesis: verum
end;

theorem :: RINFSUP1:83
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ) )
assume A1: seq is bounded ; ::_thesis: ( r = lim_inf seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) )
hence  ( r = lim_inf seq implies for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ) by Th81, Th82; ::_thesis: ( ( for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ) implies r = lim_inf seq )
assume A2: for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ) ; ::_thesis: r = lim_inf seq
then  for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds r - s < seq . (n + k) ;
then A3: r <= lim_inf seq by A1, Th82;
 for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s by A2;
then  lim_inf seq <= r by A1, Th81;
hence  r = lim_inf seq by A3, XXREAL_0:1; ::_thesis: verum
end;

theorem Th84: :: RINFSUP1:84
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) )
set seq1 = superior_realsequence seq;
assume A1: seq is bounded ; ::_thesis: ( r <= lim_sup seq iff for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )
then A2: superior_realsequence seq is bounded by Th56;
thus  ( r <= lim_sup seq implies for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) ::_thesis: ( ( for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) implies r <= lim_sup seq )
proof
assume A3: r <= lim_sup seq ; ::_thesis: for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s
let s be real number ; ::_thesis: ( 0 < s implies for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s )
assume A4: 0 < s ; ::_thesis: for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s
 for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s
proof
let n be Element of NAT ; ::_thesis: ex k being Element of NAT st seq . (n + k) > r - s
consider k being Element of NAT  such that
A5: seq . (n + k) > ((superior_realsequence seq) . n) - s by A1, A4, Th41;
 (superior_realsequence seq) . n >= r by A2, A3, Th10;
then  ((superior_realsequence seq) . n) + (seq . (n + k)) > r + (((superior_realsequence seq) . n) - s) by A5, XREAL_1:8;
then  seq . (n + k) > ((r + ((superior_realsequence seq) . n)) - s) - ((superior_realsequence seq) . n) by XREAL_1:19;
hence  ex k being Element of NAT st seq . (n + k) > r - s ; ::_thesis: verum
end;
hence  for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ; ::_thesis: verum
end;
assume A6: for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ; ::_thesis: r <= lim_sup seq
 for s being real number st 0 < s holds
lim_sup seq >= r - s
proof
let s be real number ; ::_thesis: ( 0 < s implies lim_sup seq >= r - s )
assume A7: 0 < s ; ::_thesis: lim_sup seq >= r - s
 for n being Element of NAT holds r - s <= (superior_realsequence seq) . n
proof
let n be Element of NAT ; ::_thesis: r - s <= (superior_realsequence seq) . n
consider k being Element of NAT  such that
A8: r - s < seq . (n + k) by A6, A7;
 seq . (n + k) <= (superior_realsequence seq) . n by A1, Th41;
hence  r - s <= (superior_realsequence seq) . n by A8, XXREAL_0:2; ::_thesis: verum
end;
hence  lim_sup seq >= r - s by Th10; ::_thesis: verum
end;
hence  r <= lim_sup seq by XREAL_1:57; ::_thesis: verum
end;

theorem Th85: :: RINFSUP1:85
for r being real number
for seq being Real_Sequence st seq is bounded holds
( lim_sup seq <= r iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
( lim_sup seq <= r iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( lim_sup seq <= r iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) )
set seq1 = superior_realsequence seq;
assume A1: seq is bounded ; ::_thesis: ( lim_sup seq <= r iff for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
then A2: superior_realsequence seq is bounded by Th56;
thus  ( lim_sup seq <= r implies for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) ::_thesis: ( ( for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) implies lim_sup seq <= r )
proof
assume A3: lim_sup seq <= r ; ::_thesis: for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s
 for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s
proof
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s )
assume A4: 0 < s ; ::_thesis: ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s
 ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s
proof
consider n1 being Element of NAT  such that
A5: (superior_realsequence seq) . n1 < (lower_bound (superior_realsequence seq)) + s by A2, A4, Th8;
 ((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq)) < r + ((lower_bound (superior_realsequence seq)) + s) by A3, A5, XREAL_1:8;
then  ((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq)) < (r + s) + (lower_bound (superior_realsequence seq)) ;
then A6: (((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq))) - (lower_bound (superior_realsequence seq)) < r + s by XREAL_1:19;
now__::_thesis:_for_k_being_Element_of_NAT_holds_seq_._(n1_+_k)_<_r_+_s
let k be Element of NAT ; ::_thesis: seq . (n1 + k) < r + s
 seq . (n1 + k) <= (superior_realsequence seq) . n1 by A1, Th41;
then  (seq . (n1 + k)) + ((superior_realsequence seq) . n1) < (r + s) + ((superior_realsequence seq) . n1) by A6, XREAL_1:8;
then  ((seq . (n1 + k)) + ((superior_realsequence seq) . n1)) - ((superior_realsequence seq) . n1) < r + s by XREAL_1:19;
hence  seq . (n1 + k) < r + s ; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: verum
end;
hence  for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: verum
end;
assume A7: for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: lim_sup seq <= r
 for s being real number st 0 < s holds
lim_sup seq <= r + s
proof
let s be real number ; ::_thesis: ( 0 < s implies lim_sup seq <= r + s )
assume  0 < s ; ::_thesis: lim_sup seq <= r + s
then consider n1 being Element of NAT  such that
A8: for k being Element of NAT holds seq . (n1 + k) < r + s by A7;
 for k being Element of NAT holds seq . (n1 + k) <= r + s by A8;
then A9: (superior_realsequence seq) . n1 <= r + s by A1, Th44;
 lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . n1 by A2, Th8;
hence  lim_sup seq <= r + s by A9, XXREAL_0:2; ::_thesis: verum
end;
hence  lim_sup seq <= r by XREAL_1:41; ::_thesis: verum
end;

theorem :: RINFSUP1:86
for r being real number
for seq being Real_Sequence st seq is bounded holds
( r = lim_sup seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) )
proof
let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds
( r = lim_sup seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) )
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r = lim_sup seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) ) )
assume A1: seq is bounded ; ::_thesis: ( r = lim_sup seq iff for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) )
hence  ( r = lim_sup seq implies for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) ) by Th84, Th85; ::_thesis: ( ( for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) ) implies r = lim_sup seq )
assume A2: for s being real number st 0 < s holds
( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ) ; ::_thesis: r = lim_sup seq
then  for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds seq . (n + k) < r + s ;
then A3: lim_sup seq <= r by A1, Th85;
 for s being real number st 0 < s holds
for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s by A2;
then  r <= lim_sup seq by A1, Th84;
hence  r = lim_sup seq by A3, XXREAL_0:1; ::_thesis: verum
end;

theorem :: RINFSUP1:87
for seq being Real_Sequence st seq is bounded holds
lim_inf seq <= lim_sup seq by Th55;

theorem Th88: :: RINFSUP1:88
for seq being Real_Sequence holds
( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )
proof
let seq be Real_Sequence; ::_thesis: ( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent )
thus  ( seq is bounded & lim_sup seq = lim_inf seq implies seq is convergent ) ::_thesis: ( seq is convergent implies ( seq is bounded & lim_sup seq = lim_inf seq ) )
proof
reconsider r = lower_bound (superior_realsequence seq) as real number ;
assume that
A1: seq is bounded and
A2: lim_sup seq = lim_inf seq ; ::_thesis: seq is convergent
A3: inferior_realsequence seq is bounded by A1, Th56;
A4: inferior_realsequence seq is V48() by A1, Th50;
A5: superior_realsequence seq is V49() by A1, Th51;
A6: superior_realsequence seq is bounded by A1, Th56;
 for s being real number st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s
proof
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s )
assume A7: 0 < s ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s
consider k2 being Element of NAT  such that
A8: (superior_realsequence seq) . k2 < r + s by A6, A7, Th8;
consider k1 being Element of NAT  such that
A9: r - s < (inferior_realsequence seq) . k1 by A2, A3, A7, Th7;
reconsider k = max (k1,k2) as Element of NAT ;
 k2 <= k by XXREAL_0:25;
then A10: (superior_realsequence seq) . k <= (superior_realsequence seq) . k2 by A5, SEQM_3:8;
 k1 <= k by XXREAL_0:25;
then A11: (inferior_realsequence seq) . k1 <= (inferior_realsequence seq) . k by A4, SEQM_3:6;
 ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s
proof
take  k ; ::_thesis: for m being Element of NAT st k <= m holds
abs ((seq . m) - r) < s
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((seq . m) - r) < s )
assume  k <= m ; ::_thesis: abs ((seq . m) - r) < s
then consider k3 being Nat such that
A12: m = k + k3 by NAT_1:10;
A13: k3 in NAT by ORDINAL1:def_12;
then  seq . m <= (superior_realsequence seq) . k by A1, A12, Th41;
then  seq . m <= (superior_realsequence seq) . k2 by A10, XXREAL_0:2;
then A14: seq . m < r + s by A8, XXREAL_0:2;
 (inferior_realsequence seq) . k <= seq . m by A1, A12, A13, Th40;
then  (inferior_realsequence seq) . k1 <= seq . m by A11, XXREAL_0:2;
then  r - s < seq . m by A9, XXREAL_0:2;
hence  abs ((seq . m) - r) < s by A14, Th1; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < s ; ::_thesis: verum
end;
hence  seq is convergent by SEQ_2:def_6; ::_thesis: verum
end;
assume A15: seq is convergent ; ::_thesis: ( seq is bounded & lim_sup seq = lim_inf seq )
then consider r being real number  such that
A16: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p by SEQ_2:def_6;
A17: seq is bounded by A15;
A18: for p being real number st 0 < p holds
ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) )
assume  0 < p ; ::_thesis: ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p )
then consider n being Element of NAT  such that
A19: for m being Element of NAT st n <= m holds
abs ((seq . m) - r) < p by A16;
A20: for m being Element of NAT st n <= m holds
( r - p <= seq . m & seq . m <= r + p )
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies ( r - p <= seq . m & seq . m <= r + p ) )
assume  n <= m ; ::_thesis: ( r - p <= seq . m & seq . m <= r + p )
then  abs ((seq . m) - r) < p by A19;
hence  ( r - p <= seq . m & seq . m <= r + p ) by Th1; ::_thesis: verum
end;
then  for m being Element of NAT st n <= m holds
seq . m <= r + p ;
then A21: (superior_realsequence seq) . n <= r + p by A17, Th45;
 for m being Element of NAT st n <= m holds
r - p <= seq . m by A20;
then  r - p <= (inferior_realsequence seq) . n by A17, Th43;
hence  ex n being Element of NAT st
( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A21; ::_thesis: verum
end;
A22: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A17, Th56;
A23: for p being real number st 0 < p holds
( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
proof
let p be real number ; ::_thesis: ( 0 < p implies ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) )
assume  0 < p ; ::_thesis: ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
then consider n being Element of NAT  such that
A24: ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A18;
 ( (inferior_realsequence seq) . n <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . n ) by A22, Th7, Th8;
hence  ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) by A24, XXREAL_0:2; ::_thesis: verum
end;
reconsider r = r as Real by XREAL_0:def_1;
A25: for p being real number st 0 < p holds
lower_bound (superior_realsequence seq) <= r + p by A23;
then A26: lower_bound (superior_realsequence seq) <= r by XREAL_1:41;
 for p being real number st 0 < p holds
r <= (upper_bound (inferior_realsequence seq)) + p
proof
let p be real number ; ::_thesis: ( 0 < p implies r <= (upper_bound (inferior_realsequence seq)) + p )
assume  0 < p ; ::_thesis: r <= (upper_bound (inferior_realsequence seq)) + p
then  r - p <= upper_bound (inferior_realsequence seq) by A23;
hence  r <= (upper_bound (inferior_realsequence seq)) + p by XREAL_1:20; ::_thesis: verum
end;
then A27: r <= upper_bound (inferior_realsequence seq) by XREAL_1:41;
A28: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by A15, Th55;
 lower_bound (superior_realsequence seq) <= r by A25, XREAL_1:41;
then  upper_bound (inferior_realsequence seq) <= r by A28, XXREAL_0:2;
then  r = upper_bound (inferior_realsequence seq) by A27, XXREAL_0:1;
hence  ( seq is bounded & lim_sup seq = lim_inf seq ) by A15, A28, A26, XXREAL_0:1; ::_thesis: verum
end;

theorem :: RINFSUP1:89
for seq being Real_Sequence st seq is convergent holds
( lim seq = lim_sup seq & lim seq = lim_inf seq )
proof
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies ( lim seq = lim_sup seq & lim seq = lim_inf seq ) )
reconsider r = lim seq as real number ;
assume A1: seq is convergent ; ::_thesis: ( lim seq = lim_sup seq & lim seq = lim_inf seq )
then A2: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by Th55;
A3: seq is bounded by A1;
then A4: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by Th56;
A5: for p being real number st 0 < p holds
( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
proof
let p be real number ; ::_thesis: ( 0 < p implies ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) )
assume  0 < p ; ::_thesis: ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p )
then consider k being Element of NAT  such that
A6: for m being Element of NAT st k <= m holds
abs ((seq . m) - r) < p by A1, SEQ_2:def_7;
A7: for m being Element of NAT st k <= m holds
( r - p <= seq . m & seq . m <= r + p )
proof
let m be Element of NAT ; ::_thesis: ( k <= m implies ( r - p <= seq . m & seq . m <= r + p ) )
assume  k <= m ; ::_thesis: ( r - p <= seq . m & seq . m <= r + p )
then  abs ((seq . m) - r) < p by A6;
hence  ( r - p <= seq . m & seq . m <= r + p ) by Th1; ::_thesis: verum
end;
then  for m being Element of NAT st k <= m holds
r - p <= seq . m ;
then A8: r - p <= (inferior_realsequence seq) . k by A3, Th43;
 for m being Element of NAT st k <= m holds
seq . m <= r + p by A7;
then A9: (superior_realsequence seq) . k <= r + p by A3, Th45;
 ( (inferior_realsequence seq) . k <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . k ) by A4, Th7, Th8;
hence  ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) by A8, A9, XXREAL_0:2; ::_thesis: verum
end;
A10: for p being real number st 0 < p holds
r <= (upper_bound (inferior_realsequence seq)) + p
proof
let p be real number ; ::_thesis: ( 0 < p implies r <= (upper_bound (inferior_realsequence seq)) + p )
assume  0 < p ; ::_thesis: r <= (upper_bound (inferior_realsequence seq)) + p
then  r - p <= upper_bound (inferior_realsequence seq) by A5;
hence  r <= (upper_bound (inferior_realsequence seq)) + p by XREAL_1:20; ::_thesis: verum
end;
then A11: r <= upper_bound (inferior_realsequence seq) by XREAL_1:41;
 r <= upper_bound (inferior_realsequence seq) by A10, XREAL_1:41;
then A12: r <= lower_bound (superior_realsequence seq) by A2, XXREAL_0:2;
 for p being real number st 0 < p holds
lower_bound (superior_realsequence seq) <= r + p by A5;
then A13: lower_bound (superior_realsequence seq) <= r by XREAL_1:41;
then  upper_bound (inferior_realsequence seq) <= r by A2, XXREAL_0:2;
hence  ( lim seq = lim_sup seq & lim seq = lim_inf seq ) by A13, A11, A12, XXREAL_0:1; ::_thesis: verum
end;

theorem Th90: :: RINFSUP1:90
for seq being Real_Sequence st seq is bounded holds
( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )
proof
let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) )
assume A1: seq is bounded ; ::_thesis: ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )
then  inferior_realsequence seq is bounded by Th56;
then A2: - (lim_inf seq) = - (- (lower_bound (- (inferior_realsequence seq)))) by Th13
.= lower_bound (- (- (superior_realsequence (- seq)))) by A1, Th61
.= lim_sup (- seq) ;
 superior_realsequence seq is bounded by A1, Th56;
then  - (lim_sup seq) = - (- (upper_bound (- (superior_realsequence seq)))) by Th14
.= upper_bound (- (- (inferior_realsequence (- seq)))) by A1, Th62
.= lim_inf (- seq) ;
hence  ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) by A2; ::_thesis: verum
end;

theorem :: RINFSUP1:91
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds
( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded and
A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; ::_thesis: ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 )
A4: ( superior_realsequence seq1 is convergent & inferior_realsequence seq1 is convergent ) by A1, Th57, Th58;
 superior_realsequence seq2 is bounded by A2, Th56;
then A5: lim (superior_realsequence seq2) = lower_bound (superior_realsequence seq2) by A2, Th25, Th51;
 inferior_realsequence seq1 is bounded by A1, Th56;
then A6: lim (inferior_realsequence seq1) = upper_bound (inferior_realsequence seq1) by A1, Th24, Th50;
 superior_realsequence seq1 is bounded by A1, Th56;
then A7: lim (superior_realsequence seq1) = lower_bound (superior_realsequence seq1) by A1, Th25, Th51;
A8: ( superior_realsequence seq2 is convergent & inferior_realsequence seq2 is convergent ) by A2, Th57, Th58;
 inferior_realsequence seq2 is bounded by A2, Th56;
then A9: lim (inferior_realsequence seq2) = upper_bound (inferior_realsequence seq2) by A2, Th24, Th50;
 ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) by A1, A2, A3, Th75;
hence  ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) by A4, A8, A7, A6, A5, A9, SEQ_2:18; ::_thesis: verum
end;

theorem :: RINFSUP1:92
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies ( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) ) )
assume A1: ( seq1 is bounded & seq2 is bounded ) ; ::_thesis: ( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) )
A2: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) )
set r1 = lim_sup seq1;
set r2 = lim_sup seq2;
assume that
A3: seq1 is bounded and
A4: seq2 is bounded ; ::_thesis: lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2)
 for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s
proof
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s )
assume  0 < s ; ::_thesis: ex n being Element of NAT st
for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s
then A5: 0 < s / 2 by XREAL_1:215;
then consider n1 being Element of NAT  such that
A6: for k being Element of NAT holds seq1 . (n1 + k) < (lim_sup seq1) + (s / 2) by A3, Th85;
consider n2 being Element of NAT  such that
A7: for k being Element of NAT holds seq2 . (n2 + k) < (lim_sup seq2) + (s / 2) by A4, A5, Th85;
 for k being Element of NAT holds (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s
proof
let k be Element of NAT ; ::_thesis: (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s
 ( seq1 . (n1 + (n2 + k)) < (lim_sup seq1) + (s / 2) & seq2 . (n2 + (n1 + k)) < (lim_sup seq2) + (s / 2) ) by A6, A7;
then  (seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k)) < ((lim_sup seq1) + (s / 2)) + ((lim_sup seq2) + (s / 2)) by XREAL_1:8;
hence  (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s by SEQ_1:7; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s ; ::_thesis: verum
end;
hence  lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) by A3, A4, Th85; ::_thesis: verum
end;
A8: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
(lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) )
assume that
A9: seq1 is bounded and
A10: seq2 is bounded ; ::_thesis: (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2)
 lim_sup ((seq1 + seq2) + (- seq1)) <= (lim_sup (- seq1)) + (lim_sup (seq1 + seq2)) by A2, A9, A10;
then  lim_sup ((seq1 + seq2) + (- seq1)) <= (- (lim_inf seq1)) + (lim_sup (seq1 + seq2)) by A9, Th90;
then  lim_sup ((seq2 + seq1) - seq1) <= (lim_sup (seq1 + seq2)) - (lim_inf seq1) ;
then  lim_sup seq2 <= (lim_sup (seq1 + seq2)) - (lim_inf seq1) by Th2;
hence  (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) by XREAL_1:19; ::_thesis: verum
end;
then A11: (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) by A1;
A12: (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) by A8, A1;
A13: lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) by A2, A1;
A14: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
(lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) )
set r1 = lim_inf seq1;
set r2 = lim_inf seq2;
assume that
A15: seq1 is bounded and
A16: seq2 is bounded ; ::_thesis: (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2)
 for s being real number st 0 < s holds
ex n being Element of NAT st
for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k)
proof
let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st
for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) )
assume  0 < s ; ::_thesis: ex n being Element of NAT st
for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k)
then A17: 0 < s / 2 by XREAL_1:215;
then consider n1 being Element of NAT  such that
A18: for k being Element of NAT holds (lim_inf seq1) - (s / 2) < seq1 . (n1 + k) by A15, Th82;
consider n2 being Element of NAT  such that
A19: for k being Element of NAT holds (lim_inf seq2) - (s / 2) < seq2 . (n2 + k) by A16, A17, Th82;
 for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k)
proof
let k be Element of NAT ; ::_thesis: ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k)
 ( (lim_inf seq1) - (s / 2) < seq1 . (n1 + (n2 + k)) & (lim_inf seq2) - (s / 2) < seq2 . (n2 + (n1 + k)) ) by A18, A19;
then  ((lim_inf seq1) - (s / 2)) + ((lim_inf seq2) - (s / 2)) < (seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k)) by XREAL_1:8;
hence  ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k) by SEQ_1:7; ::_thesis: verum
end;
hence  ex n being Element of NAT st
for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) ; ::_thesis: verum
end;
hence  (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) by A15, A16, Th82; ::_thesis: verum
end;
then A20: (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) by A1;
A21: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds
lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) )
assume that
A22: seq1 is bounded and
A23: seq2 is bounded ; ::_thesis: lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2)
 lim_inf ((seq1 + seq2) + (- seq2)) >= (lim_inf (seq1 + seq2)) + (lim_inf (- seq2)) by A14, A22, A23;
then  lim_inf ((seq1 + seq2) + (- seq2)) >= (lim_inf (seq1 + seq2)) + (- (lim_sup seq2)) by A23, Th90;
then  lim_inf ((seq1 + seq2) - seq2) >= (lim_inf (seq1 + seq2)) - (lim_sup seq2) ;
then  lim_inf seq1 >= (lim_inf (seq1 + seq2)) - (lim_sup seq2) by Th2;
hence  lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) by XREAL_1:20; ::_thesis: verum
end;
then A24: lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) by A1;
A25: lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) by A21, A1;
 ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) )
proof
assume A26: ( seq1 is convergent or seq2 is convergent ) ; ::_thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) )
percases ( seq1 is convergent or seq2 is convergent ) by A26;
suppose seq1 is convergent ; ::_thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) )
then  lim_inf seq1 = lim_sup seq1 by Th88;
hence  ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) by A20, A24, A11, A13, XXREAL_0:1; ::_thesis: verum
end;
suppose seq2 is convergent ; ::_thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) )
then  lim_inf seq2 = lim_sup seq2 by Th88;
hence  ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) by A20, A25, A12, A13, XXREAL_0:1; ::_thesis: verum
end;
end;
end;
hence  ( (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) & lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) & lim_inf (seq1 + seq2) <= (lim_sup seq1) + (lim_inf seq2) & (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) & (lim_sup seq1) + (lim_inf seq2) <= lim_sup (seq1 + seq2) & lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) & ( ( seq1 is convergent or seq2 is convergent ) implies ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) ) ) by A14, A21, A2, A8, A1; ::_thesis: verum
end;

theorem :: RINFSUP1:93
for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) )
A1: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) )
assume that
A2: ( seq1 is bounded & seq1 is nonnegative ) and
A3: ( seq2 is bounded & seq2 is nonnegative ) ; ::_thesis: lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2)
set seq3 = superior_realsequence seq1;
set seq4 = superior_realsequence seq2;
set seq5 = superior_realsequence (seq1 (#) seq2);
A4: superior_realsequence (seq1 (#) seq2) is convergent by A2, A3, Th58;
A5: ( lower_bound (superior_realsequence (seq1 (#) seq2)) = lim (superior_realsequence (seq1 (#) seq2)) & lower_bound (superior_realsequence seq1) = lim (superior_realsequence seq1) ) by A2, A3, Th58;
A6: lower_bound (superior_realsequence seq2) = lim (superior_realsequence seq2) by A3, Th58;
A7: for n being Element of NAT holds (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n
proof
let n be Element of NAT ; ::_thesis: (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n
 (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) by A2, A3, Th80;
hence  (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n by SEQ_1:8; ::_thesis: verum
end;
A8: ( superior_realsequence seq1 is convergent & superior_realsequence seq2 is convergent ) by A2, A3, Th58;
then  (superior_realsequence seq1) (#) (superior_realsequence seq2) is convergent ;
then  lim (superior_realsequence (seq1 (#) seq2)) <= lim ((superior_realsequence seq1) (#) (superior_realsequence seq2)) by A4, A7, SEQ_2:18;
hence  lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) by A8, A5, A6, SEQ_2:15; ::_thesis: verum
end;
 for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds
(lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2)
proof
let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) )
assume that
A9: ( seq1 is bounded & seq1 is nonnegative ) and
A10: ( seq2 is bounded & seq2 is nonnegative ) ; ::_thesis: (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2)
set seq3 = inferior_realsequence seq1;
set seq4 = inferior_realsequence seq2;
set seq5 = inferior_realsequence (seq1 (#) seq2);
A11: inferior_realsequence (seq1 (#) seq2) is convergent by A9, A10, Th57;
A12: ( upper_bound (inferior_realsequence (seq1 (#) seq2)) = lim (inferior_realsequence (seq1 (#) seq2)) & upper_bound (inferior_realsequence seq1) = lim (inferior_realsequence seq1) ) by A9, A10, Th57;
A13: upper_bound (inferior_realsequence seq2) = lim (inferior_realsequence seq2) by A10, Th57;
A14: for n being Element of NAT holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n
proof
let n be Element of NAT ; ::_thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n
 (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A9, A10, Th79;
hence  (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n by SEQ_1:8; ::_thesis: verum
end;
A15: ( inferior_realsequence seq1 is convergent & inferior_realsequence seq2 is convergent ) by A9, A10, Th57;
then  (inferior_realsequence seq1) (#) (inferior_realsequence seq2) is convergent ;
then  lim (inferior_realsequence (seq1 (#) seq2)) >= lim ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) by A11, A14, SEQ_2:18;
hence  (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) by A15, A12, A13, SEQ_2:15; ::_thesis: verum
end;
hence  ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) ) by A1; ::_thesis: verum
end;