let X be ComplexUnitarySpace; 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; ( seq1 is convergent & seq2 is convergent implies seq1 - seq2 is convergent )
assume that
A1:
seq1 is convergent
and
A2:
seq2 is convergent
; seq1 - seq2 is convergent
consider g1 being Point of X such that
A3:
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq1 . n),g1) < r
by A1;
consider g2 being Point of X such that
A4:
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq2 . n),g2) < r
by A2;
take g = g1 - g2; CLVECT_2:def 1 for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (((seq1 - seq2) . n),g) < r
let r be Real; ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist (((seq1 - seq2) . n),g) < r )
assume A5:
r > 0
; ex m being Nat st
for n being Nat st n >= m holds
dist (((seq1 - seq2) . n),g) < r
then consider m1 being Nat such that
A6:
for n being Nat st n >= m1 holds
dist ((seq1 . n),g1) < r / 2
by A3, XREAL_1:215;
consider m2 being Nat such that
A7:
for n being Nat st n >= m2 holds
dist ((seq2 . n),g2) < r / 2
by A4, A5, XREAL_1:215;
take k = m1 + m2; for n being Nat st n >= k holds
dist (((seq1 - seq2) . n),g) < r
let n be Nat; ( n >= k implies dist (((seq1 - seq2) . n),g) < r )
assume A8:
n >= k
; dist (((seq1 - seq2) . n),g) < r
k >= m2
by NAT_1:12;
then
n >= m2
by A8, XXREAL_0:2;
then A9:
dist ((seq2 . n),g2) < r / 2
by A7;
dist (((seq1 - seq2) . n),g) = dist (((seq1 . n) - (seq2 . n)),(g1 - g2))
by NORMSP_1:def 3;
then A10:
dist (((seq1 - seq2) . n),g) <= (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2))
by CSSPACE:57;
m1 + m2 >= m1
by NAT_1:12;
then
n >= m1
by A8, XXREAL_0:2;
then
dist ((seq1 . n),g1) < r / 2
by A6;
then
(dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) < (r / 2) + (r / 2)
by A9, XREAL_1:8;
hence
dist (((seq1 - seq2) . n),g) < r
by A10, XXREAL_0:2; verum