let X be RealUnitarySpace; 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; ( 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
; lim (seq1 - seq2) = (lim seq1) - (lim seq2)
set g2 = lim seq2;
set g1 = lim seq1;
set g = (lim seq1) - (lim seq2);
A3:
now 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))) < rlet r be
Real;
( 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
;
ex k being set st
for n being Nat st n >= k holds
dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < rthen 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;
for n being Nat st n >= k holds
dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < rlet n be
Nat;
( n >= k implies dist (((seq1 - seq2) . n),((lim seq1) - (lim seq2))) < r )assume A7:
n >= k
;
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 3;
then A9:
dist (
((seq1 - seq2) . n),
((lim seq1) - (lim seq2)))
<= (dist ((seq1 . n),(lim seq1))) + (dist ((seq2 . n),(lim seq2)))
by BHSP_1:41;
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;
verum end;
seq1 - seq2 is convergent
by A1, A2, Th4;
hence
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
by A3, Def2; verum