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 )

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

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

hence
q is convergent
by SEQ_2:def 6; :: thesis: ( lim p = lim q & lim r = lim q )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

end;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;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

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