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 ; :: according to FUNCT_2:def 8 :: thesis: (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 ;
:: thesis: verum

end;

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