let seq be ExtREAL_sequence; :: thesis: ( seq is non-decreasing implies ( seq is convergent & lim seq = sup seq ) )

assume A1: seq is non-decreasing ; :: thesis: ( seq is convergent & lim seq = sup seq )

assume A1: seq is non-decreasing ; :: thesis: ( seq is convergent & lim seq = sup seq )

per cases
( for n being Element of NAT holds seq . n <= -infty or ex n being Element of NAT st not seq . n <= -infty )
;

end;

suppose A2:
for n being Element of NAT holds seq . n <= -infty
; :: thesis: ( seq is convergent & lim seq = sup seq )

A6: seq is convergent_to_-infty by A2, Th33;

hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq

then rng seq = {-infty} by A5, XBOOLE_0:def 10;

then sup seq = -infty by XXREAL_2:11;

hence lim seq = sup seq by A6, A7, MESFUNC5:def 12; :: thesis: verum

end;

now :: thesis: for y being object st y in {-infty} holds

y in rng seq

then A5:
{-infty} c= rng seq
;y in rng seq

let y be object ; :: thesis: ( y in {-infty} implies y in rng seq )

assume y in {-infty} ; :: thesis: y in rng seq

then A3: y = -infty by TARSKI:def 1;

end;assume y in {-infty} ; :: thesis: y in rng seq

then A3: y = -infty by TARSKI:def 1;

now :: thesis: y in rng seq

hence
y in rng seq
; :: thesis: verumassume A4:
not y in rng seq
; :: thesis: contradiction

end;now :: thesis: for n being Element of NAT holds contradiction

hence
contradiction
; :: thesis: verumlet n be Element of NAT ; :: thesis: contradiction

n in NAT ;

then n in dom seq by FUNCT_2:def 1;

then seq . n <> -infty by A3, A4, FUNCT_1:def 3;

hence contradiction by A2, XXREAL_0:6; :: thesis: verum

end;n in NAT ;

then n in dom seq by FUNCT_2:def 1;

then seq . n <> -infty by A3, A4, FUNCT_1:def 3;

hence contradiction by A2, XXREAL_0:6; :: thesis: verum

A6: seq is convergent_to_-infty by A2, Th33;

hence A7: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq

now :: thesis: for y being object st y in rng seq holds

y in {-infty}

then
rng seq c= {-infty}
;y in {-infty}

let y be object ; :: thesis: ( y in rng seq implies y in {-infty} )

assume y in rng seq ; :: thesis: y in {-infty}

then ex x being object st

( x in dom seq & seq . x = y ) by FUNCT_1:def 3;

then y = -infty by A2, XXREAL_0:6;

hence y in {-infty} by TARSKI:def 1; :: thesis: verum

end;assume y in rng seq ; :: thesis: y in {-infty}

then ex x being object st

( x in dom seq & seq . x = y ) by FUNCT_1:def 3;

then y = -infty by A2, XXREAL_0:6;

hence y in {-infty} by TARSKI:def 1; :: thesis: verum

then rng seq = {-infty} by A5, XBOOLE_0:def 10;

then sup seq = -infty by XXREAL_2:11;

hence lim seq = sup seq by A6, A7, MESFUNC5:def 12; :: thesis: verum

suppose
not for n being Element of NAT holds seq . n <= -infty
; :: thesis: ( seq is convergent & lim seq = sup seq )

then consider k being Element of NAT such that

A8: -infty < seq . k ;

end;A8: -infty < seq . k ;

per cases
( +infty <> sup seq or +infty = sup seq )
;

end;

suppose A9:
+infty <> sup seq
; :: thesis: ( seq is convergent & lim seq = sup seq )

set seq0 = seq ^\ k;

A10: sup seq = sup (seq ^\ k) by A1, Th26;

A14: sup (rng (seq ^\ k)) is UpperBound of rng (seq ^\ k) by XXREAL_2:def 3;

seq . k <= sup seq by Th23;

then seq . k < +infty by A9, XXREAL_0:2, XXREAL_0:4;

then A15: seq ^\ k is bounded_below by A1, A8, Th31;

then rng (seq ^\ k) is bounded_below ;

then -infty < inf (rng (seq ^\ k)) by A11, XXREAL_0:12, XXREAL_2:58;

then sup (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;

then rng (seq ^\ k) is bounded_above by A14, XXREAL_2:def 10;

then seq ^\ k is bounded_above ;

then A16: seq ^\ k is bounded by A15;

A17: seq ^\ k is non-decreasing by A1, Th26;

then A18: lim (seq ^\ k) = sup (seq ^\ k) by A16, Lm4;

seq ^\ k is convergent by A17, A16, Lm4;

hence ( seq is convergent & lim seq = sup seq ) by A10, A18, Th17; :: thesis: verum

end;A10: sup seq = sup (seq ^\ k) by A1, Th26;

A11: now :: thesis: not rng (seq ^\ k) = {+infty}

A13:
inf (seq ^\ k) <= sup (seq ^\ k)
by Th24;assume
rng (seq ^\ k) = {+infty}
; :: thesis: contradiction

then A12: +infty in rng (seq ^\ k) by TARSKI:def 1;

+infty is UpperBound of rng (seq ^\ k) by XXREAL_2:41;

hence contradiction by A9, A10, A12, XXREAL_2:55; :: thesis: verum

end;then A12: +infty in rng (seq ^\ k) by TARSKI:def 1;

+infty is UpperBound of rng (seq ^\ k) by XXREAL_2:41;

hence contradiction by A9, A10, A12, XXREAL_2:55; :: thesis: verum

A14: sup (rng (seq ^\ k)) is UpperBound of rng (seq ^\ k) by XXREAL_2:def 3;

seq . k <= sup seq by Th23;

then seq . k < +infty by A9, XXREAL_0:2, XXREAL_0:4;

then A15: seq ^\ k is bounded_below by A1, A8, Th31;

then rng (seq ^\ k) is bounded_below ;

then -infty < inf (rng (seq ^\ k)) by A11, XXREAL_0:12, XXREAL_2:58;

then sup (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14;

then rng (seq ^\ k) is bounded_above by A14, XXREAL_2:def 10;

then seq ^\ k is bounded_above ;

then A16: seq ^\ k is bounded by A15;

A17: seq ^\ k is non-decreasing by A1, Th26;

then A18: lim (seq ^\ k) = sup (seq ^\ k) by A16, Lm4;

seq ^\ k is convergent by A17, A16, Lm4;

hence ( seq is convergent & lim seq = sup seq ) by A10, A18, Th17; :: thesis: verum

suppose A19:
+infty = sup seq
; :: thesis: ( seq is convergent & lim seq = sup seq )

then
seq is convergent_to_+infty
by A1, Th35;

hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq

thus lim seq = sup seq by A1, A19, Th35; :: thesis: verum

end;hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = sup seq

thus lim seq = sup seq by A1, A19, Th35; :: thesis: verum