let c, d be Real; :: thesis: ( 0 < c implies for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p )
set f = rseq (1,0,c,d);
assume A1: 0 < c ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p )
assume A2: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
set f1 = rseq (0,(- d),(c * c),(c * d));
lim (rseq (0,(- d),(c * c),(c * d))) = 0 by A1, Th10;
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.(((rseq (0,(- d),(c * c),(c * d))) . m) - 0).| < p by A2, SEQ_2:def 7;
consider m1 being Nat such that
A4: 0 < (c * m1) + d by A1, Th1;
reconsider mm = max (m1,(n + 1)) as Nat by TARSKI:1;
take mm ; :: thesis: for m being Nat st mm <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
let m be Nat; :: thesis: ( mm <= m implies |.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p )
assume A5: mm <= m ; :: thesis: |.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
m1 <= mm by XXREAL_0:25;
then m1 <= m by A5, XXREAL_0:2;
then c * m1 <= c * m by A1, XREAL_1:64;
then A6: (c * m1) + d <= (c * m) + d by XREAL_1:6;
A7: n + 0 <= n + 1 by XREAL_1:6;
n + 1 <= mm by XXREAL_0:25;
then n <= mm by A7, XXREAL_0:2;
then A8: n <= m by A5, XXREAL_0:2;
((rseq (1,0,c,d)) . m) - (1 / c) = (((1 * m) + 0) / ((c * m) + d)) - (1 / c) by Th5
.= ((m * c) - (1 * ((c * m) + d))) / (((c * m) + d) * c) by A1, A6, A4, XCMPLX_1:130
.= ((0 * m) + (- d)) / (((c * c) * m) + (c * d))
.= ((rseq (0,(- d),(c * c),(c * d))) . m) - 0 by Th5 ;
hence |.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p by A3, A8; :: thesis: verum