let X be ComplexUnitarySpace; for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
let x be Point of X; for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
let seq be sequence of X; ( seq is convergent implies lim (seq + x) = (lim seq) + x )
set g = lim seq;
assume A1:
seq is convergent
; lim (seq + x) = (lim seq) + x
A2:
now for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < rlet r be
Real;
( r > 0 implies ex k being Nat st
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < r )assume
r > 0
;
ex k being Nat st
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < rthen consider m1 being
Nat such that A3:
for
n being
Nat st
n >= m1 holds
dist (
(seq . n),
(lim seq))
< r
by A1, Def2;
take k =
m1;
for n being Nat st n >= k holds
dist (((seq + x) . n),((lim seq) + x)) < rlet n be
Nat;
( n >= k implies dist (((seq + x) . n),((lim seq) + x)) < r )assume
n >= k
;
dist (((seq + x) . n),((lim seq) + x)) < rthen A4:
dist (
(seq . n),
(lim seq))
< r
by A3;
dist (
(seq . n),
(lim seq)) =
dist (
((seq . n) - (- x)),
((lim seq) - (- x)))
by CSSPACE:58
.=
dist (
((seq . n) + (- (- x))),
((lim seq) - (- x)))
by RLVECT_1:def 11
.=
dist (
((seq . n) + x),
((lim seq) - (- x)))
by RLVECT_1:17
.=
dist (
((seq . n) + x),
((lim seq) + (- (- x))))
by RLVECT_1:def 11
.=
dist (
((seq . n) + x),
((lim seq) + x))
by RLVECT_1:17
;
hence
dist (
((seq + x) . n),
((lim seq) + x))
< r
by A4, BHSP_1:def 6;
verum end;
seq + x is convergent
by A1, Th7;
hence
lim (seq + x) = (lim seq) + x
by A2, Def2; verum