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

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