let k be Nat; :: thesis: ( aseq k is convergent & lim (aseq k) = 1 )
A1: for eps being Real st 0 < eps holds
ex N being Nat st
for n being Nat st N <= n holds
|.(((aseq k) . n) - 1).| < eps

proof

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

end;

thus aseq k is convergent by A1; :: thesis: lim (aseq k) = 1
hence lim (aseq k) = 1 by A1, SEQ_2:def 7; :: thesis: verum