let N be Nat; :: thesis: for seq being Real_Sequence of N st seq is convergent holds
lim (- seq) = - (lim seq)
let seq be Real_Sequence of N; :: thesis: ( seq is convergent implies lim (- seq) = - (lim seq) )
assume seq is convergent ; :: thesis: lim (- seq) = - (lim seq)
then lim ((- 1) * seq) = (- 1) * (lim seq) by Th39
.= - (1 * (lim seq)) by RLVECT_1:79
.= - (lim seq) by RLVECT_1:def 8 ;
hence lim (- seq) = - (lim seq) by Th11; :: thesis: verum