theorem Th41: :: TOPRNS_1:41
for N being Nat
for seq being Real_Sequence of N st seq is convergent holds
lim (- seq) = - (lim seq)