let X be ComplexUnitarySpace; :: thesis: 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; :: thesis: for seq being sequence of X st seq is convergent holds
seq + x is convergent
let seq be sequence of X; :: thesis: ( seq is convergent implies seq + x is convergent )
assume seq is convergent ; :: thesis: 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 Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),g < r by Def1;
take g + x ; :: according to CLVECT_2:def 1 :: thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq + x) . n),(g + x) < r
let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq + x) . n),(g + x) < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist ((seq + x) . n),(g + x) < r
then consider m1 being Element of NAT such that
A2: for n being Element of NAT st n >= m1 holds
dist (seq . n),g < r by A1;
take k = m1; :: thesis: for n being Element of NAT st n >= k holds
dist ((seq + x) . n),(g + x) < r
let n be Element of NAT ; :: thesis: ( n >= k implies dist ((seq + x) . n),(g + x) < r )
assume n >= k ; :: thesis: dist ((seq + x) . n),(g + x) < r
then A3: dist (seq . n),g < r by A2;
dist ((seq . n) + x),(g + x) <= (dist (seq . n),g) + (dist x,x) by CSSPACE:59;
then dist ((seq . n) + x),(g + x) <= (dist (seq . n),g) + 0 by CSSPACE:53;
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 12; :: thesis: verum