let c, d be Real; ( c < 0 implies lim (rseq (0,1,c,d)) = 0 )
set f = rseq (0,1,c,d);
assume A1:
c < 0
; 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
;
verum