let d be Real; :: thesis: for c being non zero Real holds rseq (1,0,c,d) is convergent
let c be non zero Real; :: thesis: rseq (1,0,c,d) is convergent

per cases ( 0 < c or c < 0 ) ;

suppose 0 < c ; :: thesis: rseq (1,0,c,d) is convergent

hence rseq (1,0,c,d) is convergent by Lm10; :: thesis: verum

end;

suppose A1: c < 0 ; :: thesis: rseq (1,0,c,d) is convergent

A2: rseq (1,0,c,d) = (- 1) (#) (rseq (1,0,(- c),(- d))) by Th8;
rseq (1,0,(- c),(- d)) is convergent by A1, Lm10;
hence rseq (1,0,c,d) is convergent by A2; :: thesis: verum

end;

end;