theorem Th16: :: CLVECT_2:16

for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)