let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 - seq2 is convergent
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent )
assume that
A1: seq1 is convergent and
A2: seq2 is convergent ; :: thesis: seq1 - seq2 is convergent
consider g1 being Point of X such that
A3: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq1 . n),g1 < r by A1, Def1;
consider g2 being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq2 . n),g2 < r by A2, Def1;
take g = g1 - g2; :: according to BHSP_2:def 1 :: thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 - seq2) . n),g < r
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 ((seq1 - seq2) . n),g < r )
assume A5: r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq1 - seq2) . n),g < r
then r / 2 > 0 by XREAL_1:217;
then consider m1 being Element of NAT such that
A6: for n being Element of NAT st n >= m1 holds
dist (seq1 . n),g1 < r / 2 by A3;
consider m2 being Element of NAT such that
A7: for n being Element of NAT st n >= m2 holds
dist (seq2 . n),g2 < r / 2 by A4, A5, XREAL_1:217;
take k = m1 + m2; :: thesis: for n being Element of NAT st n >= k holds
dist ((seq1 - seq2) . n),g < r
let n be Element of NAT ; :: thesis: ( n >= k implies dist ((seq1 - seq2) . n),g < r )
assume A8: n >= k ; :: thesis: dist ((seq1 - seq2) . n),g < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A8, XXREAL_0:2;
then A9: dist (seq1 . n),g1 < r / 2 by A6;
k >= m2 by NAT_1:12;
then n >= m2 by A8, XXREAL_0:2;
then dist (seq2 . n),g2 < r / 2 by A7;
then A10: (dist (seq1 . n),g1) + (dist (seq2 . n),g2) < (r / 2) + (r / 2) by A9, XREAL_1:10;
dist ((seq1 - seq2) . n),g = dist ((seq1 . n) - (seq2 . n)),(g1 - g2) by NORMSP_1:def 6;
then dist ((seq1 - seq2) . n),g <= (dist (seq1 . n),g1) + (dist (seq2 . n),g2) by BHSP_1:48;
hence dist ((seq1 - seq2) . n),g < r by A10, XXREAL_0:2; :: thesis: verum