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;