let f, g be Real_Sequence; :: thesis: for N being Element of NAT
for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds
f . n = g . n ) holds
( g is convergent & lim g = c )
let N be Element of NAT ; :: thesis: for c being Real st f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds
f . n = g . n ) holds
( g is convergent & lim g = c )
let c be Real; :: thesis: ( f is convergent & lim f = c & ( for n being Element of NAT st n >= N holds
f . n = g . n ) implies ( g is convergent & lim g = c ) )
assume that
A1: f is convergent and
A2: lim f = c and
A3: for n being Element of NAT st n >= N holds
f . n = g . n ; :: thesis: ( g is convergent & lim g = c )

A4: now :: thesis: for p being Real st p > 0 holds
ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((g . n) - c).| < p

let p be Real; :: thesis: ( p > 0 implies ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((g . n) - c).| < p )
assume p > 0 ; :: thesis: ex N1 being Nat st
for n being Nat st n >= N1 holds
|.((g . n) - c).| < p
then consider M being Nat such that
A5: for n being Nat st n >= M holds
|.((f . n) - c).| < p by A1, A2, SEQ_2:def 7;
reconsider N1 = max (N,M) as Nat by TARSKI:1;
A6: N1 >= N by XXREAL_0:25;
take N1 = N1; :: thesis: for n being Nat st n >= N1 holds
|.((g . n) - c).| < p
let n be Nat; :: thesis: ( n >= N1 implies |.((g . n) - c).| < p )
A7: n in NAT by ORDINAL1:def 12;
assume A8: n >= N1 ; :: thesis: |.((g . n) - c).| < p
N1 >= M by XXREAL_0:25;
then n >= M by A8, XXREAL_0:2;
then |.((f . n) - c).| < p by A5;
hence |.((g . n) - c).| < p by A3, A6, A8, XXREAL_0:2, A7; :: thesis: verum

end;

hence g is convergent by SEQ_2:def 6; :: thesis: lim g = c
hence lim g = c by A4, SEQ_2:def 7; :: thesis: verum