theorem :: CLVECT_2:38

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
( dist ((z * seq),(z * g)) is convergent & lim (dist ((z * seq),(z * g))) = 0 )