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

let e be real number ; :: thesis: ( 0 < e implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e )
assume A7: 0 < e ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e
then consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
abs ((p . m) - (lim p)) < e by A1, SEQ_2:def 7;
consider n2 being Element of NAT such that
A9: for m being Element of NAT st n2 <= m holds
abs ((r . m) - (lim r)) < e by A2, A7, SEQ_2:def 7;
reconsider n = max n1,n2 as Element of NAT by ORDINAL1:def 13;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e
thus for m being Element of NAT st n <= m holds
abs ((q . m) - (lim p)) < e :: thesis: verum

proof

let m be Element of NAT ; :: thesis: ( n <= m implies abs ((q . m) - (lim p)) < e )
assume A10: n <= m ; :: thesis: abs ((q . m) - (lim p)) < e
n1 <= n by XXREAL_0:25;
then n1 <= m by A10, XXREAL_0:2;
then abs ((p . m) - (lim p)) < e by A8;
then p . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:8;
then p . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by RCOMP_1:def 2;
then A11: ex z being Real st
( z = p . m & (lim p) - e < z & z < (lim p) + e ) ;
p . m <= q . m by A4;
then A12: (lim p) - e < q . m by A11, XXREAL_0:2;
n2 <= n by XXREAL_0:25;
then n2 <= m by A10, XXREAL_0:2;
then abs ((r . m) - (lim r)) < e by A9;
then r . m in ].((lim r) - e),((lim r) + e).[ by RCOMP_1:8;
then r . m in { z where z is Real : ( (lim r) - e < z & z < (lim r) + e ) } by RCOMP_1:def 2;
then A13: ex z being Real st
( z = r . m & (lim r) - e < z & z < (lim r) + e ) ;
q . m <= r . m by A5;
then q . m < (lim p) + e by A3, A13, XXREAL_0:2;
then q . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by A12;
then q . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:def 2;
hence abs ((q . m) - (lim p)) < e by RCOMP_1:8; :: 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