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

proof

assume not seq is convergent_to_-infty ; :: thesis: contradiction
then consider g being real number such that
A3: ( g < 0 & ( for n being Nat ex m being Nat st
( n <= m & g < seq . m ) ) ) by MESFUNC5:def 10;
for y being ext-real number st y in rng seq holds
g <= y

proof

let y be ext-real number ; :: thesis: ( y in rng seq implies g <= y )
assume y in rng seq ; :: thesis: g <= y
then consider n being set such that
A4: ( n in NAT & y = seq . n ) by FUNCT_2:17;
reconsider n = n as Element of NAT by A4;
consider m being Nat such that
A5: ( n <= m & g < seq . m ) by A3;
m is Element of NAT by ORDINAL1:def 13;
then seq . m <= seq . n by A1, A5, Th7;
hence g <= y by A4, A5, XXREAL_0:2; :: thesis: verum

end;

then g is LowerBound of rng seq by XXREAL_2:def 2;
then A6: g <= inf (rng seq) by XXREAL_2:def 4;
g in REAL by XREAL_0:def 1;
hence contradiction by A1, A6, XXREAL_0:12; :: thesis: verum

end;

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