let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent )
assume that
A1:
seq1 is convergent
and
A2:
seq1 is_compared_to seq2
; :: thesis: seq2 is convergent
now let r be
Real;
:: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq2 . n),(lim seq1) < r )assume
r > 0
;
:: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq2 . n),(lim seq1) < rthen A3:
r / 2
> 0
by XREAL_1:217;
then consider m1 being
Element of
NAT such that A4:
for
n being
Element of
NAT st
n >= m1 holds
dist (seq1 . n),
(lim seq1) < r / 2
by A1, BHSP_2:def 2;
consider m2 being
Element of
NAT such that A5:
for
n being
Element of
NAT st
n >= m2 holds
dist (seq1 . n),
(seq2 . n) < r / 2
by A2, A3, Def2;
take m =
m1 + m2;
:: thesis: for n being Element of NAT st n >= m holds
dist (seq2 . n),(lim seq1) < rlet n be
Element of
NAT ;
:: thesis: ( n >= m implies dist (seq2 . n),(lim seq1) < r )assume A6:
n >= m
;
:: thesis: dist (seq2 . n),(lim seq1) < r
m1 + m2 >= m1
by NAT_1:12;
then
n >= m1
by A6, XXREAL_0:2;
then A7:
dist (seq1 . n),
(lim seq1) < r / 2
by A4;
m >= m2
by NAT_1:12;
then
n >= m2
by A6, XXREAL_0:2;
then
dist (seq1 . n),
(seq2 . n) < r / 2
by A5;
then A8:
(dist (seq2 . n),(seq1 . n)) + (dist (seq1 . n),(lim seq1)) < (r / 2) + (r / 2)
by A7, XREAL_1:10;
dist (seq2 . n),
(lim seq1) <= (dist (seq2 . n),(seq1 . n)) + (dist (seq1 . n),(lim seq1))
by BHSP_1:42;
hence
dist (seq2 . n),
(lim seq1) < r
by A8, XXREAL_0:2;
:: thesis: verum end;
hence
seq2 is convergent
by BHSP_2:def 1; :: thesis: verum