let seq be ExtREAL_sequence; :: thesis: for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds

( rseq is convergent & lim seq = lim rseq )

let rseq be Real_Sequence; :: thesis: ( seq = rseq & seq is convergent_to_finite_number implies ( rseq is convergent & lim seq = lim rseq ) )

assume that

A1: seq = rseq and

A2: seq is convergent_to_finite_number ; :: thesis: ( rseq is convergent & lim seq = lim rseq )

A3: ( not lim seq = +infty or not seq is convergent_to_+infty ) by A2, MESFUNC5:50;

A4: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A2, MESFUNC5:51;

seq is convergent by A2, MESFUNC5:def 11;

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;

A7: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((rseq . m) - g).| < p

hence ( rseq is convergent & lim seq = lim rseq ) by A5, A7, SEQ_2:def 7; :: thesis: verum

( rseq is convergent & lim seq = lim rseq )

let rseq be Real_Sequence; :: thesis: ( seq = rseq & seq is convergent_to_finite_number implies ( rseq is convergent & lim seq = lim rseq ) )

assume that

A1: seq = rseq and

A2: seq is convergent_to_finite_number ; :: thesis: ( rseq is convergent & lim seq = lim rseq )

A3: ( not lim seq = +infty or not seq is convergent_to_+infty ) by A2, MESFUNC5:50;

A4: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A2, MESFUNC5:51;

seq is convergent by A2, MESFUNC5:def 11;

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;

A7: for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((rseq . m) - g).| < p

proof

then
rseq is convergent
by SEQ_2:def 6;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.((rseq . m) - g).| < p )

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((rseq . m) - g).| < p

then consider n being Nat such that

A8: for m being Nat st n <= m holds

|.((seq . m) - (lim seq)).| < p by A6;

reconsider N = n as Element of NAT by ORDINAL1:def 12;

take N ; :: thesis: for m being Nat st N <= m holds

|.((rseq . m) - g).| < p

end;for m being Nat st n <= m holds

|.((rseq . m) - g).| < p )

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.((rseq . m) - g).| < p

then consider n being Nat such that

A8: for m being Nat st n <= m holds

|.((seq . m) - (lim seq)).| < p by A6;

reconsider N = n as Element of NAT by ORDINAL1:def 12;

take N ; :: thesis: for m being Nat st N <= m holds

|.((rseq . m) - g).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( N <= m implies |.((rseq . m) - g).| < p )

assume N <= m ; :: thesis: |.((rseq . m) - g).| < p

then A9: |.((seq . m) - (lim seq)).| < p by A8;

(rseq . m) - g = (seq . m) - (lim seq) by A1, A5, SUPINF_2:3;

hence |.((rseq . m) - g).| < p by A9, EXTREAL1:12; :: thesis: verum

end;assume N <= m ; :: thesis: |.((rseq . m) - g).| < p

then A9: |.((seq . m) - (lim seq)).| < p by A8;

(rseq . m) - g = (seq . m) - (lim seq) by A1, A5, SUPINF_2:3;

hence |.((rseq . m) - g).| < p by A9, EXTREAL1:12; :: thesis: verum

hence ( rseq is convergent & lim seq = lim rseq ) by A5, A7, SEQ_2:def 7; :: thesis: verum