let seq be ExtREAL_sequence; :: thesis: ( ( for n being Element of NAT holds seq . n <= -infty ) implies seq is convergent_to_-infty )

assume A1: for n being Element of NAT holds seq . n <= -infty ; :: thesis: seq is convergent_to_-infty

assume A1: for n being Element of NAT holds seq . n <= -infty ; :: thesis: seq is convergent_to_-infty

now :: thesis: for g being Real st g < 0 holds

ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

hence
seq is convergent_to_-infty
by MESFUNC5:def 10; :: thesis: verumex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

for m being Nat st n <= m holds

seq . m <= g ; :: thesis: verum

end;for m being Nat st n <= m holds

seq . m <= g )

assume g < 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

seq . m <= g

now :: thesis: for m being Nat st 0 <= m holds

seq . m <= g

hence
ex n being Nat st seq . m <= g

let m be Nat; :: thesis: ( 0 <= m implies seq . m <= g )

assume 0 <= m ; :: thesis: seq . m <= g

m is Element of NAT by ORDINAL1:def 12;

then A2: seq . m <= -infty by A1;

-infty <= g by XXREAL_0:5;

hence seq . m <= g by A2, XXREAL_0:2; :: thesis: verum

end;assume 0 <= m ; :: thesis: seq . m <= g

m is Element of NAT by ORDINAL1:def 12;

then A2: seq . m <= -infty by A1;

-infty <= g by XXREAL_0:5;

hence seq . m <= g by A2, XXREAL_0:2; :: thesis: verum

for m being Nat st n <= m holds

seq . m <= g ; :: thesis: verum