theorem Th15: :: CLVECT_2:15

for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)