let c, d be Real; :: thesis: ( 0 < c implies lim (rseq (0,1,c,d)) = 0 )
set f = rseq (0,1,c,d);
assume A1: 0 < c ; :: thesis: lim (rseq (0,1,c,d)) = 0
then A2: rseq (0,1,c,d) is convergent by Lm5;
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p by A1, Lm4;
hence lim (rseq (0,1,c,d)) = 0 by A2, SEQ_2:def 7; :: thesis: verum