let c, d be Real; :: thesis: rseq (0,1,c,d) is convergent
set f = rseq (0,1,c,d);

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

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

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

end;

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

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

end;

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

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

end;

end;