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

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

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

now :: thesis: for m being Nat st 0 <= m holds
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;

hence ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m ; :: thesis: verum

end;

hence seq is convergent_to_+infty by MESFUNC5:def 9; :: thesis: verum