theorem :: NFCONT_2:16

for K, L, e being Real st 0 < K & K < 1 & 0 < e holds
ex n being Nat st |.(L * (K to_power n)).| < e by Lm2;