let d be Real; :: thesis: for c being non zero Real holds lim (rseq (1,0,c,d)) = 1 / c
let c be non zero Real; :: thesis: lim (rseq (1,0,c,d)) = 1 / c
per cases ( 0 < c or c < 0 ) ;
suppose 0 < c ; :: thesis: lim (rseq (1,0,c,d)) = 1 / c
hence lim (rseq (1,0,c,d)) = 1 / c by Lm11; :: thesis: verum
end;
suppose A1: c < 0 ; :: thesis: lim (rseq (1,0,c,d)) = 1 / c
set f = rseq (1,0,c,d);
set f1 = rseq (1,0,(- c),(- d));
A2: rseq (1,0,c,d) = (- 1) (#) (rseq (1,0,(- c),(- d))) by Th8;
lim (rseq (1,0,(- c),(- d))) = 1 / (- c) by A1, Lm11;
hence lim (rseq (1,0,c,d)) = (- 1) / (- c) by A2, A1, Lm10, SEQ_2:8
.= 1 / c by XCMPLX_1:191 ;
:: thesis: verum
end;
end;