let seq, seq1 be Real_Sequence; :: thesis: ( seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n implies lim seq = lim seq1 )
assume A1: seq is convergent ; :: thesis: ( for k being Nat ex n being Nat st
( k <= n & not seq1 . n = seq . n ) or lim seq = lim seq1 )
given k being Nat such that A2: for n being Nat st k <= n holds
seq1 . n = seq . n ; :: thesis: lim seq = lim seq1

A3: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Nat such that
A4: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A1, SEQ_2:def 7;

A5: now :: thesis: ( n1 <= k implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )

assume A6: n1 <= k ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
take n = k; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A7: n <= m ; :: thesis: |.((seq1 . m) - (lim seq)).| < p
then n1 <= m by A6, XXREAL_0:2;
then |.((seq . m) - (lim seq)).| < p by A4;
hence |.((seq1 . m) - (lim seq)).| < p by A2, A7; :: thesis: verum

end;

now :: thesis: ( k <= n1 implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )

assume A8: k <= n1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
take n = n1; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A9: n <= m ; :: thesis: |.((seq1 . m) - (lim seq)).| < p
then seq1 . m = seq . m by A2, A8, XXREAL_0:2;
hence |.((seq1 . m) - (lim seq)).| < p by A4, A9; :: thesis: verum

end;

hence ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p by A5; :: thesis: verum

end;

seq1 is convergent by A1, A2, Th18;
hence lim seq = lim seq1 by A3, SEQ_2:def 7; :: thesis: verum