let a, b, d be Real; :: thesis: for c being non zero Real holds lim (rseq (a,b,c,d)) = a / c
let c be non zero Real; :: thesis: lim (rseq (a,b,c,d)) = a / c
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;

A4: lim (rseq (1,0,c,d)) = 1 / c by Lm13;
A5: lim (rseq (0,b,c,d)) = 0 by Th10;
thus lim (rseq (a,b,c,d)) = (lim (a (#) (rseq (1,0,c,d)))) + (lim (rseq (0,b,c,d))) by A1, SEQ_2:6
.= a / c by A4, A5, SEQ_2:8 ; :: thesis: verum