let c, d be Real; :: thesis: ( c < 0 implies lim (rseq (0,1,c,d)) = 0 )
set f = rseq (0,1,c,d);
assume A1: c < 0 ; :: thesis: lim (rseq (0,1,c,d)) = 0
set f1 = rseq (0,1,(- c),(- d));
A2: rseq (0,1,c,d) = (- 1) (#) (rseq (0,1,(- c),(- d))) by Th7;
lim (rseq (0,1,(- c),(- d))) = 0 by A1, Lm7;
hence 0 = (- 1) * (lim (rseq (0,1,(- c),(- d))))
.= lim (rseq (0,1,c,d)) by A1, A2, Lm5, SEQ_2:8 ;
:: thesis: verum