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

assume that

A1: seq is non-decreasing and

A2: +infty = sup seq ; :: thesis: ( seq is convergent_to_+infty & lim seq = +infty )

A3: seq is convergent_to_+infty

hence ( seq is convergent_to_+infty & lim seq = +infty ) by A3, MESFUNC5:def 12; :: thesis: verum

assume that

A1: seq is non-decreasing and

A2: +infty = sup seq ; :: thesis: ( seq is convergent_to_+infty & lim seq = +infty )

A3: seq is convergent_to_+infty

proof

then
seq is convergent
by MESFUNC5:def 11;
assume
not seq is convergent_to_+infty
; :: thesis: contradiction

then consider g being Real such that

0 < g and

A4: for n being Nat ex m being Nat st

( n <= m & seq . m < g ) by MESFUNC5:def 9;

for y being ExtReal st y in rng seq holds

y <= g

then A9: sup (rng seq) <= g by XXREAL_2:def 3;

g in REAL by XREAL_0:def 1;

hence contradiction by A2, A9, XXREAL_0:9; :: thesis: verum

end;then consider g being Real such that

0 < g and

A4: for n being Nat ex m being Nat st

( n <= m & seq . m < g ) by MESFUNC5:def 9;

for y being ExtReal st y in rng seq holds

y <= g

proof

then
g is UpperBound of rng seq
by XXREAL_2:def 1;
let y be ExtReal; :: thesis: ( y in rng seq implies y <= g )

assume y in rng seq ; :: thesis: y <= g

then consider n being object such that

A5: n in NAT and

A6: y = seq . n by FUNCT_2:11;

reconsider n = n as Element of NAT by A5;

consider m being Nat such that

A7: n <= m and

A8: seq . m < g by A4;

seq . n <= seq . m by A1, A7, Th7;

hence y <= g by A6, A8, XXREAL_0:2; :: thesis: verum

end;assume y in rng seq ; :: thesis: y <= g

then consider n being object such that

A5: n in NAT and

A6: y = seq . n by FUNCT_2:11;

reconsider n = n as Element of NAT by A5;

consider m being Nat such that

A7: n <= m and

A8: seq . m < g by A4;

seq . n <= seq . m by A1, A7, Th7;

hence y <= g by A6, A8, XXREAL_0:2; :: thesis: verum

then A9: sup (rng seq) <= g by XXREAL_2:def 3;

g in REAL by XREAL_0:def 1;

hence contradiction by A2, A9, XXREAL_0:9; :: thesis: verum

hence ( seq is convergent_to_+infty & lim seq = +infty ) by A3, MESFUNC5:def 12; :: thesis: verum