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