let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds

lim (seq1 + seq2) = (lim seq1) + (lim seq2)

let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2) = (lim seq1) + (lim seq2) )

assume that

A1: seq1 is convergent and

A2: seq2 is convergent ; :: thesis: lim (seq1 + seq2) = (lim seq1) + (lim seq2)

set g2 = lim seq2;

set g1 = lim seq1;

set g = (lim seq1) + (lim seq2);

hence lim (seq1 + seq2) = (lim seq1) + (lim seq2) by A3, Def2; :: thesis: verum

lim (seq1 + seq2) = (lim seq1) + (lim seq2)

let seq1, seq2 be sequence of X; :: thesis: ( seq1 is convergent & seq2 is convergent implies lim (seq1 + seq2) = (lim seq1) + (lim seq2) )

assume that

A1: seq1 is convergent and

A2: seq2 is convergent ; :: thesis: lim (seq1 + seq2) = (lim seq1) + (lim seq2)

set g2 = lim seq2;

set g1 = lim seq1;

set g = (lim seq1) + (lim seq2);

A3: now :: thesis: for r being Real st r > 0 holds

ex k being set st

for n being Nat st n >= k holds

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

seq1 + seq2 is convergent
by A1, A2, Th3;ex k being set st

for n being Nat st n >= k holds

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

let r be Real; :: thesis: ( r > 0 implies ex k being set st

for n being Nat st n >= k holds

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

assume r > 0 ; :: thesis: ex k being set st

for n being Nat st n >= k holds

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

then A4: r / 2 > 0 by XREAL_1:215;

then consider m1 being Nat such that

A5: for n being Nat st n >= m1 holds

dist ((seq1 . n),(lim seq1)) < r / 2 by A1, Def2;

consider m2 being Nat such that

A6: for n being Nat st n >= m2 holds

dist ((seq2 . n),(lim seq2)) < r / 2 by A2, A4, Def2;

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

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

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

assume A7: n >= k ; :: thesis: dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r

k >= m2 by NAT_1:12;

then n >= m2 by A7, XXREAL_0:2;

then A8: dist ((seq2 . n),(lim seq2)) < r / 2 by A6;

dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) = dist (((seq1 . n) + (seq2 . n)),((lim seq1) + (lim seq2))) by NORMSP_1:def 2;

then A9: dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) <= (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) by BHSP_1:40;

m1 + m2 >= m1 by NAT_1:12;

then n >= m1 by A7, XXREAL_0:2;

then dist ((seq1 . n),(lim seq1)) < r / 2 by A5;

then (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) < (r / 2) + (r / 2) by A8, XREAL_1:8;

hence dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r by A9, XXREAL_0:2; :: thesis: verum

end;for n being Nat st n >= k holds

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

assume r > 0 ; :: thesis: ex k being set st

for n being Nat st n >= k holds

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

then A4: r / 2 > 0 by XREAL_1:215;

then consider m1 being Nat such that

A5: for n being Nat st n >= m1 holds

dist ((seq1 . n),(lim seq1)) < r / 2 by A1, Def2;

consider m2 being Nat such that

A6: for n being Nat st n >= m2 holds

dist ((seq2 . n),(lim seq2)) < r / 2 by A2, A4, Def2;

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

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

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

assume A7: n >= k ; :: thesis: dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r

k >= m2 by NAT_1:12;

then n >= m2 by A7, XXREAL_0:2;

then A8: dist ((seq2 . n),(lim seq2)) < r / 2 by A6;

dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) = dist (((seq1 . n) + (seq2 . n)),((lim seq1) + (lim seq2))) by NORMSP_1:def 2;

then A9: dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) <= (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) by BHSP_1:40;

m1 + m2 >= m1 by NAT_1:12;

then n >= m1 by A7, XXREAL_0:2;

then dist ((seq1 . n),(lim seq1)) < r / 2 by A5;

then (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2))) < (r / 2) + (r / 2) by A8, XREAL_1:8;

hence dist (((seq1 + seq2) . n),((lim seq1) + (lim seq2))) < r by A9, XXREAL_0:2; :: thesis: verum

hence lim (seq1 + seq2) = (lim seq1) + (lim seq2) by A3, Def2; :: thesis: verum