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 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; :: according to BHSP_2:def 1 :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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;

reconsider k = m1 + m2 as Nat ;

take k ; :: thesis: for n being Nat st n >= k holds

dist (((seq1 + seq2) . n),g) < r

let n be Nat; :: thesis: ( n >= k implies dist (((seq1 + seq2) . n),g) < r )

assume A8: n >= k ; :: thesis: 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 2;

then A10: dist (((seq1 + seq2) . n),g) <= (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) by BHSP_1:40;

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; :: thesis: verum

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 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; :: according to BHSP_2:def 1 :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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;

reconsider k = m1 + m2 as Nat ;

take k ; :: thesis: for n being Nat st n >= k holds

dist (((seq1 + seq2) . n),g) < r

let n be Nat; :: thesis: ( n >= k implies dist (((seq1 + seq2) . n),g) < r )

assume A8: n >= k ; :: thesis: 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 2;

then A10: dist (((seq1 + seq2) . n),g) <= (dist ((seq1 . n),g1)) + (dist ((seq2 . n),g2)) by BHSP_1:40;

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; :: thesis: verum