theorem :: BHSP_2:34

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