let eps be Real; :: thesis: ( 0 < eps implies ex N being Nat st
for n being Nat st N <= n holds
|.(((aseq k) . n) - 1).| < eps )
assume A2: eps > 0 ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
|.(((aseq k) . n) - 1).| < eps
consider N being Nat such that
A3: N > k / eps by SEQ_4:3;
take N ; :: thesis: for n being Nat st N <= n holds
|.(((aseq k) . n) - 1).| < eps
let n be Nat; :: thesis: ( N <= n implies |.(((aseq k) . n) - 1).| < eps )
assume A4: n >= N ; :: thesis: |.(((aseq k) . n) - 1).| < eps
then n > k / eps by A3, XXREAL_0:2;
then (k / eps) * eps < n * eps by A2, XREAL_1:68;
then A5: k < n * eps by A2, XCMPLX_1:87;
A6: n > 0 by A2, A3, A4;
then |.(((aseq k) . n) - 1).| = |.((1 - (k / n)) - 1).| by Th7
.= |.(- (k / n)).|
.= |.(k / n).| by COMPLEX1:52
.= k / n by ABSVALUE:def 1 ;
hence |.(((aseq k) . n) - 1).| < eps by A6, A5, XREAL_1:83; :: thesis: verum