theorem :: CLVECT_2:29

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