theorem Th22: :: BHSP_2:22

for X being RealUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )