let K, L, e be real number ; :: thesis: ( 0 < K & K < 1 & 0 < e implies ex n being Element of NAT st abs (L * (K to_power n)) < e )
assume that
A1:
0 < K
and
A2:
K < 1
and
A3:
0 < e
; :: thesis: ex n being Element of NAT st abs (L * (K to_power n)) < e
deffunc H1( Element of NAT ) -> set = K to_power ($1 + 1);
consider rseq being Real_Sequence such that
A4:
for n being Element of NAT holds rseq . n = H1(n)
from SEQ_1:sch 1();
A5:
( rseq is convergent & lim rseq = 0 )
by A1, A2, A4, SERIES_1:1;
then A6:
L (#) rseq is convergent
by SEQ_2:21;
lim (L (#) rseq) =
L * (lim rseq)
by A5, SEQ_2:22
.=
0
by A5
;
then consider n being Element of NAT such that
A7:
for m being Element of NAT st n <= m holds
abs (((L (#) rseq) . m) - 0 ) < e
by A3, A6, SEQ_2:def 7;
abs (((L (#) rseq) . n) - 0 ) < e
by A7;
then
abs (L * (rseq . n)) < e
by SEQ_1:13;
then
abs (L * (K to_power (n + 1))) < e
by A4;
hence
ex n being Element of NAT st abs (L * (K to_power n)) < e
; :: thesis: verum