let seq be ExtREAL_sequence; :: thesis: ( seq is non-increasing & -infty = inf seq implies ( seq is convergent_to_-infty & lim seq = -infty ) )

assume that

A1: seq is non-increasing and

A2: -infty = inf 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-increasing and

A2: -infty = inf 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

g < 0 and

A4: for n being Nat ex m being Nat st

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

for y being ExtReal st y in rng seq holds

g <= y

then A9: g <= inf (rng seq) by XXREAL_2:def 4;

g in REAL by XREAL_0:def 1;

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

end;then consider g being Real such that

g < 0 and

A4: for n being Nat ex m being Nat st

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

for y being ExtReal st y in rng seq holds

g <= y

proof

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

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

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: g < seq . m by A4;

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

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

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

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: g < seq . m by A4;

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

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

then A9: g <= inf (rng seq) by XXREAL_2:def 4;

g in REAL by XREAL_0:def 1;

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

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