set f1 = rseq (0,1,c,d);
A1: rseq (0,b,c,d) = b (#) (rseq (0,1,c,d))

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (rseq (0,b,c,d)) . n = (b (#) (rseq (0,1,c,d))) . n
(rseq (0,1,c,d)) . n = ((0 * n) + 1) / ((c * n) + d) by Th5;
hence (b (#) (rseq (0,1,c,d))) . n = ((0 * n) + b) / ((c * n) + d) by VALUED_1:6
.= (rseq (0,b,c,d)) . n by Th5 ;
:: thesis: verum

end;

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