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₁( Nat) -> object = L to_power ($1 + 1);
consider rseq being Real_Sequence such that
A2: for n being Nat holds rseq . n = H₁(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