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

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

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

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

ex n being Nat st

for m being Nat st n <= m holds

g <= seq . m

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

for m being Nat st n <= m holds

g <= seq . m

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

for m being Nat st n <= m holds

g <= seq . m )

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

for m being Nat st n <= m holds

g <= seq . m

for m being Nat st n <= m holds

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

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

g <= seq . m )

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

for m being Nat st n <= m holds

g <= seq . m

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

g <= seq . m

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

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

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

m is Element of NAT by ORDINAL1:def 12;

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

g <= +infty by XXREAL_0:3;

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

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

m is Element of NAT by ORDINAL1:def 12;

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

g <= +infty by XXREAL_0:3;

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

for m being Nat st n <= m holds

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