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 AS: ( 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 ) ) ; :: thesis: ( q is convergent & lim p = lim q & lim r = lim q )

X: 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 AS1: 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
consider n1 being Element of NAT such that
P1: for m being Element of NAT st n1 <= m holds
abs ((p . m) - (lim p)) < e by SEQ_2:def 7, AS, AS1;
consider n2 being Element of NAT such that
P2: for m being Element of NAT st n2 <= m holds
abs ((r . m) - (lim r)) < e by SEQ_2:def 7, AS, AS1;
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 AS2: n <= m ; :: thesis: abs ((q . m) - (lim p)) < e
n1 <= n by XXREAL_0:25;
then n1 <= m by AS2, XXREAL_0:2;
then A1: abs ((p . m) - (lim p)) < e by P1;
n2 <= n by XXREAL_0:25;
then n2 <= m by AS2, XXREAL_0:2;
then A2: abs ((r . m) - (lim r)) < e by P2;
p . m in ].((lim p) - e),((lim p) + e).[ by RCOMP_1:8, A1;
then p . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by RCOMP_1:def 2;
then A3: ex z being Real st
( z = p . m & (lim p) - e < z & z < (lim p) + e ) ;
p . m <= q . m by AS;
then A4: (lim p) - e < q . m by XXREAL_0:2, A3;
r . m in ].((lim r) - e),((lim r) + e).[ by RCOMP_1:8, A2;
then r . m in { z where z is Real : ( (lim r) - e < z & z < (lim r) + e ) } by RCOMP_1:def 2;
then A5: ex z being Real st
( z = r . m & (lim r) - e < z & z < (lim r) + e ) ;
q . m <= r . m by AS;
then q . m < (lim p) + e by XXREAL_0:2, A5, AS;
then q . m in { z where z is Real : ( (lim p) - e < z & z < (lim p) + e ) } by A4;
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 X, SEQ_2:def 7, AS; :: thesis: verum