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

suppose A2: seq is convergent_to_finite_number ; :: thesis: ex b₁ being R_eal st
( ex g being Real st
( b₁ = 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₁).| < p ) & seq is convergent_to_finite_number ) or ( b₁ = +infty & seq is convergent_to_+infty ) or ( b₁ = -infty & seq is convergent_to_-infty ) )

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;

suppose ( seq is convergent_to_+infty or seq is convergent_to_-infty ) ; :: thesis: ex b₁ being R_eal st
( ex g being Real st
( b₁ = 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₁).| < p ) & seq is convergent_to_finite_number ) or ( b₁ = +infty & seq is convergent_to_+infty ) or ( b₁ = -infty & seq is convergent_to_-infty ) )

hence ex b₁ being R_eal st
( ex g being Real st
( b₁ = 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₁).| < p ) & seq is convergent_to_finite_number ) or ( b₁ = +infty & seq is convergent_to_+infty ) or ( b₁ = -infty & seq is convergent_to_-infty ) ) ; :: thesis: verum

end;

end;