let seq, seq9, seq1 be Real_Sequence; ( seq is convergent & seq9 is convergent & ( for n being Nat holds
( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 implies seq1 is convergent )
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
; seq1 is convergent
take
lim seq
; SEQ_2:def 6 for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let p be Real; ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p )
assume A5:
0 < p
; ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
then consider n1 being Nat such that
A6:
for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p
by A1, Def6;
consider n2 being Nat such that
A7:
for m being Nat st n2 <= m holds
|.((seq9 . m) - (lim seq)).| < p
by A2, A4, A5, Def6;
take n = n1 + n2; for m being Nat st n <= m holds
|.((seq1 . m) - (lim seq)).| < p
let m be Nat; ( n <= m implies |.((seq1 . m) - (lim seq)).| < p )
assume A8:
n <= m
; |.((seq1 . m) - (lim seq)).| < p
n2 <= n
by NAT_1:12;
then
n2 <= m
by A8, XXREAL_0:2;
then
|.((seq9 . m) - (lim seq)).| < p
by A7;
then A9:
(seq9 . m) - (lim seq) < p
by Th1;
n1 <= n1 + n2
by NAT_1:12;
then
n1 <= m
by A8, XXREAL_0:2;
then
|.((seq . m) - (lim seq)).| < p
by A6;
then A10:
- 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 A11:
- p < (seq1 . m) - (lim seq)
by A10, 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 A9, XXREAL_0:2;
hence
|.((seq1 . m) - (lim seq)).| < p
by A11, Th1; verum