let b, d be Real; :: thesis: for c being non zero Real holds lim (rseq (0,b,c,d)) = 0
let c be non zero Real; :: thesis: lim (rseq (0,b,c,d)) = 0
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;
( c < 0 or 0 < c ) ;
then lim (rseq (0,1,c,d)) = 0 by Lm7, Lm8;
hence 0 = b * (lim (rseq (0,1,c,d)))
.= lim (rseq (0,b,c,d)) by A1, SEQ_2:8 ;
:: thesis: verum