theorem Th33: :: BHSP_2:33

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
( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )