theorem :: BHSP_2:39

for X being RealUnitarySpace
for x, g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist ((seq + x),(g + x)) is convergent & lim (dist ((seq + x),(g + x))) = 0 )