let X be RealUnitarySpace; :: 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 Nat st
for n being Nat st n >= m holds
dist ((seq . n),g) < r ;
take g + x ; :: according to BHSP_2:def 1 :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: for n being Nat st n >= k holds
dist (((seq + x) . n),(g + x)) < r
let n be Nat; :: thesis: ( n >= k implies dist (((seq + x) . n),(g + x)) < r )
dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + (dist (x,x)) by BHSP_1:40;
then A3: dist (((seq . n) + x),(g + x)) <= (dist ((seq . n),g)) + 0 by BHSP_1:34;
assume n >= k ; :: thesis: 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; :: thesis: verum