theorem :: CLVECT_2:32

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