let K, L, e be Real; :: thesis: ( 0 < K & K < 1 & 0 < e implies ex n being Nat st |.(L * (K to_power n)).| < e )
assume that
A1: ( 0 < K & K < 1 ) and
A2: 0 < e ; :: thesis: ex n being Nat st |.(L * (K to_power n)).| < e
deffunc H₁( Nat) -> object = K to_power ($1 + 1);
consider rseq being Real_Sequence such that
A3: for n being Nat holds rseq . n = H₁(n) from SEQ_1:sch 1();
A4: L (#) rseq is convergent by A1, A3, SEQ_2:7, SERIES_1:1;
A5: lim rseq = 0 by A1, A3, SERIES_1:1;
lim (L (#) rseq) = L * (lim rseq) by A1, A3, SEQ_2:8, SERIES_1:1
.= 0 by A5 ;
then consider n being Nat such that
A6: for m being Nat st n <= m holds
|.(((L (#) rseq) . m) - 0).| < e by A2, A4, SEQ_2:def 7;
|.(((L (#) rseq) . n) - 0).| < e by A6;
then |.(L * (rseq . n)).| < e by SEQ_1:9;
then |.(L * (K to_power (n + 1))).| < e by A3;
hence ex n being Nat st |.(L * (K to_power n)).| < e ; :: thesis: verum