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_{1}( Nat) -> object = K to_power ($1 + 1);

consider rseq being Real_Sequence such that

A3: for n being Nat holds rseq . n = H_{1}(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

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

consider rseq being Real_Sequence such that

A3: for n being Nat holds rseq . n = H

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