per cases
( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty )
by A1;

end;

suppose A2:
seq is convergent_to_finite_number
; :: thesis: ex b_{1} being R_eal st

( ex g being Real st

( b_{1} = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < p ) & seq is convergent_to_finite_number ) or ( b_{1} = +infty & seq is convergent_to_+infty ) or ( b_{1} = -infty & seq is convergent_to_-infty ) )

( ex g being Real st

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

then consider g being Real such that

A3: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ;

reconsider g = g as R_eal by XXREAL_0:def 1;

take g ; :: thesis: ( ex g being Real st

( g = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ) & seq is convergent_to_finite_number ) or ( g = +infty & seq is convergent_to_+infty ) or ( g = -infty & seq is convergent_to_-infty ) )

thus ( ex g being Real st

( g = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ) & seq is convergent_to_finite_number ) or ( g = +infty & seq is convergent_to_+infty ) or ( g = -infty & seq is convergent_to_-infty ) ) by A2, A3; :: thesis: verum

end;A3: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ;

reconsider g = g as R_eal by XXREAL_0:def 1;

take g ; :: thesis: ( ex g being Real st

( g = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ) & seq is convergent_to_finite_number ) or ( g = +infty & seq is convergent_to_+infty ) or ( g = -infty & seq is convergent_to_-infty ) )

thus ( ex g being Real st

( g = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - g).| < p ) & seq is convergent_to_finite_number ) or ( g = +infty & seq is convergent_to_+infty ) or ( g = -infty & seq is convergent_to_-infty ) ) by A2, A3; :: thesis: verum

suppose
( seq is convergent_to_+infty or seq is convergent_to_-infty )
; :: thesis: ex b_{1} being R_eal st

( ex g being Real st

( b_{1} = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < p ) & seq is convergent_to_finite_number ) or ( b_{1} = +infty & seq is convergent_to_+infty ) or ( b_{1} = -infty & seq is convergent_to_-infty ) )

( ex g being Real st

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b

hence
ex b_{1} being R_eal st

( ex g being Real st

( b_{1} = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b_{1}).| < p ) & seq is convergent_to_finite_number ) or ( b_{1} = +infty & seq is convergent_to_+infty ) or ( b_{1} = -infty & seq is convergent_to_-infty ) )
; :: thesis: verum

end;( ex g being Real st

( b

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - b