let X be ComplexUnitarySpace; for x being Point of X
for seq being sequence of X st seq is convergent holds
seq + x is convergent
let x be Point of X; for seq being sequence of X st seq is convergent holds
seq + x is convergent
let seq be sequence of X; ( seq is convergent implies seq + x is convergent )
assume
seq is convergent
; seq + x is convergent
then consider g being Point of X such that
A1:
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),g) < r
;
take
g + x
; CLVECT_2:def 1 for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (((seq + x) . n),(g + x)) < r
let r be Real; ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
dist (((seq + x) . n),(g + x)) < r )
assume
r > 0
; ex m being Nat st
for n being Nat st n >= m holds
dist (((seq + x) . n),(g + x)) < r
then consider m1 being Nat such that
A2:
for n being Nat st n >= m1 holds
dist ((seq . n),g) < r
by A1;
take k = m1; for n being Nat st n >= k holds
dist (((seq + x) . n),(g + x)) < r
let n be Nat; ( n >= k implies dist (((seq + x) . n),(g + x)) < r )
dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + (dist (x,x))
by CSSPACE:56;
then A3:
dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + 0
by CSSPACE:50;
assume
n >= k
; dist (((seq + x) . n),(g + x)) < r
then
dist ((seq . n),g) < r
by A2;
then
dist (((seq . n) + x),(g + x)) < r
by A3, XXREAL_0:2;
hence
dist (((seq + x) . n),(g + x)) < r
by BHSP_1:def 6; verum