theorem :: CLVECT_2:31

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