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