set f2 = rseq (1,0,c,d);
set f3 = rseq (0,b,c,d);
A1:
rseq (a,b,c,d) = (a (#) (rseq (1,0,c,d))) + (rseq (0,b,c,d))
proof
let n be
Element of
NAT ;
FUNCT_2:def 8 (rseq (a,b,c,d)) . n = ((a (#) (rseq (1,0,c,d))) + (rseq (0,b,c,d))) . n
A2:
(rseq (1,0,c,d)) . n = ((1 * n) + 0) / ((c * n) + d)
by Th5;
A3:
(rseq (0,b,c,d)) . n = ((0 * n) + b) / ((c * n) + d)
by Th5;
(a (#) (rseq (1,0,c,d))) . n = a * ((rseq (1,0,c,d)) . n)
by VALUED_1:6;
hence ((a (#) (rseq (1,0,c,d))) + (rseq (0,b,c,d))) . n =
(a * ((rseq (1,0,c,d)) . n)) + ((rseq (0,b,c,d)) . n)
by VALUED_1:1
.=
((a * n) + b) / ((c * n) + d)
by A2, A3
.=
(rseq (a,b,c,d)) . n
by Th5
;
verum
end;
rseq (1,0,c,d) is convergent
by Lm12;
hence
rseq (a,b,c,d) is convergent
by A1; verum