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