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);

A3: now

let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((seq1 - seq2) . n),((lim seq1) - (lim seq2)) < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist ((seq1 - seq2) . n),((lim seq1) - (lim seq2)) < r
then A4: r / 2 > 0 by XREAL_1:217;
then consider m1 being Element of NAT such that
A5: for n being Element of NAT st n >= m1 holds
dist (seq1 . n),(lim seq1) < r / 2 by A1, Def2;
consider m2 being Element of NAT such that
A6: for n being Element of NAT st n >= m2 holds
dist (seq2 . n),(lim seq2) < r / 2 by A2, A4, Def2;
take k = m1 + m2; :: thesis: for n being Element of NAT st n >= k holds
dist ((seq1 - seq2) . n),((lim seq1) - (lim seq2)) < r
let n be Element of 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 6;
then A9: dist ((seq1 - seq2) . n),((lim seq1) - (lim seq2)) <= (dist (seq1 . n),(lim seq1)) + (dist (seq2 . n),(lim seq2)) by BHSP_1:48;
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:10;
hence dist ((seq1 - seq2) . n),((lim seq1) - (lim seq2)) < r by A9, XXREAL_0:2; :: thesis: verum

end;

seq1 - seq2 is convergent by A1, A2, Th4;
hence lim (seq1 - seq2) = (lim seq1) - (lim seq2) by A3, Def2; :: thesis: verum