let L be Real; :: thesis: ( 0 < L & L < 1 implies for s being Real st 0 < s holds

ex n being Nat st L to_power n < s )

assume A1: ( 0 < L & L < 1 ) ; :: thesis: for s being Real st 0 < s holds

ex n being Nat st L to_power n < s

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st L to_power n < s )

deffunc H_{1}( Nat) -> object = L to_power ($1 + 1);

consider rseq being Real_Sequence such that

A2: for n being Nat holds rseq . n = H_{1}(n)
from SEQ_1:sch 1();

assume A3: 0 < s ; :: thesis: ex n being Nat st L to_power n < s

( rseq is convergent & lim rseq = 0 ) by A1, A2, SERIES_1:1;

then consider n being Nat such that

A4: for m being Nat st n <= m holds

|.((rseq . m) - 0).| < s by A3, SEQ_2:def 7;

take n + 1 ; :: thesis: L to_power (n + 1) < s

A5: 0 < L to_power (n + 1) by A1, Th2;

|.((rseq . n) - 0).| = |.(L to_power (n + 1)).| by A2

.= L to_power (n + 1) by A5, ABSVALUE:def 1 ;

hence L to_power (n + 1) < s by A4; :: thesis: verum

ex n being Nat st L to_power n < s )

assume A1: ( 0 < L & L < 1 ) ; :: thesis: for s being Real st 0 < s holds

ex n being Nat st L to_power n < s

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st L to_power n < s )

deffunc H

consider rseq being Real_Sequence such that

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

assume A3: 0 < s ; :: thesis: ex n being Nat st L to_power n < s

( rseq is convergent & lim rseq = 0 ) by A1, A2, SERIES_1:1;

then consider n being Nat such that

A4: for m being Nat st n <= m holds

|.((rseq . m) - 0).| < s by A3, SEQ_2:def 7;

take n + 1 ; :: thesis: L to_power (n + 1) < s

A5: 0 < L to_power (n + 1) by A1, Th2;

|.((rseq . n) - 0).| = |.(L to_power (n + 1)).| by A2

.= L to_power (n + 1) by A5, ABSVALUE:def 1 ;

hence L to_power (n + 1) < s by A4; :: thesis: verum