let seq be ExtREAL_sequence; :: thesis: ( ( seq is convergent_to_finite_number implies ex g being Real st
( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) ) & ( seq is convergent_to_+infty implies lim seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty ) )

A1: now :: thesis: ( seq is convergent_to_finite_number implies ex g, g being Real st
( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) )

assume A2: seq is convergent_to_finite_number ; :: thesis: ex g, g being Real st
( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) )
then A3: not seq is convergent_to_+infty by MESFUNC5:50;
A4: not seq is convergent_to_-infty by A2, MESFUNC5:51;
seq is convergent by A2;
then consider g being Real such that
A5: lim seq = g and
A6: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p and
seq is convergent_to_finite_number by A3, A4, MESFUNC5:def 12;
take g = g; :: thesis: ex g being Real st
( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) )
thus ex g being Real st
( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) by A5, A6; :: thesis: verum

end;

A7: now :: thesis: ( seq is convergent_to_-infty implies lim seq = -infty )

assume A8: seq is convergent_to_-infty ; :: thesis: lim seq = -infty
then seq is convergent ;
hence lim seq = -infty by A8, MESFUNC5:def 12; :: thesis: verum

end;

now :: thesis: ( seq is convergent_to_+infty implies lim seq = +infty )

assume A9: seq is convergent_to_+infty ; :: thesis: lim seq = +infty
then seq is convergent ;
hence lim seq = +infty by A9, MESFUNC5:def 12; :: thesis: verum

end;

hence ( ( seq is convergent_to_finite_number implies ex g being Real st
( lim seq = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) ) & ( seq is convergent_to_+infty implies lim seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty ) ) by A1, A7; :: thesis: verum