let seq, seq9, seq1 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent & ( for n being Nat holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 implies lim seq1 = lim seq )
assume that
A1: seq is convergent and
A2: seq9 is convergent and
A3: for n being Nat holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) and
A4: lim seq = lim seq9 ; :: thesis: lim seq1 = lim seq
A5: seq1 is convergent by A1, A2, A3, A4, Th19;

now :: thesis: for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being set st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume A6: 0 < p ; :: thesis: ex n being set st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Nat such that
A7: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p by A1, Def6;
consider n2 being Nat such that
A8: for m being Nat st n2 <= m holds
|.((seq9 . m) - (lim seq)).| < p by A2, A4, A6, Def6;
take n = n1 + n2; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A9: n <= m ; :: thesis: |.((seq1 . m) - (lim seq)).| < p
n2 <= n by NAT_1:12;
then n2 <= m by A9, XXREAL_0:2;
then |.((seq9 . m) - (lim seq)).| < p by A8;
then A10: (seq9 . m) - (lim seq) < p by Th1;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A9, XXREAL_0:2;
then |.((seq . m) - (lim seq)).| < p by A7;
then A11: - p < (seq . m) - (lim seq) by Th1;
seq . m <= seq1 . m by A3;
then (seq . m) - (lim seq) <= (seq1 . m) - (lim seq) by XREAL_1:9;
then A12: - p < (seq1 . m) - (lim seq) by A11, XXREAL_0:2;
seq1 . m <= seq9 . m by A3;
then (seq1 . m) - (lim seq) <= (seq9 . m) - (lim seq) by XREAL_1:9;
then (seq1 . m) - (lim seq) < p by A10, XXREAL_0:2;
hence |.((seq1 . m) - (lim seq)).| < p by A12, Th1; :: thesis: verum

end;

hence lim seq1 = lim seq by A5, Def6; :: thesis: verum