let p, q, r be Real_Sequence; :: thesis: ( p is convergent & r is convergent & lim p = lim r & ( for i being Element of NAT holds p . i <= q . i ) & ( for i being Element of NAT holds q . i <= r . i ) implies ( q is convergent & lim p = lim q & lim r = lim q ) )
assume that
A1: p is convergent and
A2: r is convergent and
A3: lim p = lim r and
A4: for i being Element of NAT holds p . i <= q . i and
A5: for i being Element of NAT holds q . i <= r . i ; :: thesis: ( q is convergent & lim p = lim q & lim r = lim q )

A6: now :: thesis: for e being Real st 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
|.((q . m) - (lim p)).| < e

let e be Real; :: thesis: ( 0 < e implies ex n being Nat st
for m being Nat st n <= m holds
|.((q . m) - (lim p)).| < e )
assume A7: 0 < e ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((q . m) - (lim p)).| < e
then consider n1 being Nat such that
A8: for m being Nat st n1 <= m holds
|.((p . m) - (lim p)).| < e by A1, SEQ_2:def 7;
consider n2 being Nat such that
A9: for m being Nat st n2 <= m holds
|.((r . m) - (lim r)).| < e by A2, A7, SEQ_2:def 7;
reconsider n = max (n1,n2) as Nat by TARSKI:1;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((q . m) - (lim p)).| < e
thus for m being Nat st n <= m holds
|.((q . m) - (lim p)).| < e :: thesis: verum

proof

let m be Nat; :: thesis: ( n <= m implies |.((q . m) - (lim p)).| < e )
assume A10: n <= m ; :: thesis: |.((q . m) - (lim p)).| < e
A11: m in NAT by ORDINAL1:def 12;
n1 <= n by XXREAL_0:25;
then n1 <= m by A10, XXREAL_0:2;
then |.((p . m) - (lim p)).| < e by A8;
then p . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:1;
then p . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by RCOMP_1:def 2;
then A12: ex z being Real st
( z = p . m & (lim p) - e < z & z < (lim p) + e ) ;
p . m <= q . m by A4, A11;
then A13: (lim p) - e < q . m by A12, XXREAL_0:2;
n2 <= n by XXREAL_0:25;
then n2 <= m by A10, XXREAL_0:2;
then |.((r . m) - (lim r)).| < e by A9;
then r . m in ].((lim r) - e),((lim r) + e).[ by RCOMP_1:1;
then r . m in { z where z is Real : ( (lim r) - e < z & z < (lim r) + e ) } by RCOMP_1:def 2;
then A14: ex z being Real st
( z = r . m & (lim r) - e < z & z < (lim r) + e ) ;
q . m <= r . m by A5, A11;
then q . m < (lim p) + e by A3, A14, XXREAL_0:2;
then q . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by A13;
then q . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:def 2;
hence |.((q . m) - (lim p)).| < e by RCOMP_1:1; :: thesis: verum

end;

end;

hence q is convergent by SEQ_2:def 6; :: thesis: ( lim p = lim q & lim r = lim q )
hence ( lim q = lim p & lim q = lim r ) by A3, A6, SEQ_2:def 7; :: thesis: verum