theorem :: CLVECT_2:30

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