theorem Th15: :: BHSP_2:15

for X being RealUnitarySpace
for a being Real
for seq being sequence of X st seq is convergent holds
lim (a * seq) = a * (lim seq)