defpred S₁[ R_eal] means ( ex g being real number st
( $1 = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - $1).| < p ) & seq is convergent_to_finite_number ) or ( $1 = +infty & seq is convergent_to_+infty ) or ( $1 = -infty & seq is convergent_to_-infty ) );

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

suppose A2: seq is convergent_to_finite_number ; :: thesis: ex b₁ being R_eal st
( ex g being real number st
( b₁ = g & ( for p being real number 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 ex g being real number st
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL g)).| < p by Def8;
hence ex b₁ being R_eal st
( ex g being real number st
( b₁ = g & ( for p being real number 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 ) ) by A2; :: 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 number st
( b₁ = g & ( for p being real number 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 number st
( b₁ = g & ( for p being real number 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;