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

let p be real number ; :: thesis: ( p > 0 implies ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((g . n) - c) < p )
assume p > 0 ; :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((g . n) - c) < p
then consider M being Element of NAT such that
A5: for n being Element of NAT st n >= M holds
abs ((f . n) - c) < p by A1, A2, SEQ_2:def 7;
set N1 = max N,M;
A6: max N,M >= N by XXREAL_0:25;
take N1 = max N,M; :: thesis: for n being Element of NAT st n >= N1 holds
abs ((g . n) - c) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs ((g . n) - c) < p )
assume A7: n >= N1 ; :: thesis: abs ((g . n) - c) < p
N1 >= M by XXREAL_0:25;
then n >= M by A7, XXREAL_0:2;
then abs ((f . n) - c) < p by A5;
hence abs ((g . n) - c) < p by A3, A6, A7, XXREAL_0:2; :: 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