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 ;
FUNCT_2:def 8 (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
;
verum
end;
rseq (0,1,c,d) is convergent
by Lm6;
hence
rseq (0,b,c,d) is convergent
by A1; verum