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 ;
then (k / eps) * eps < n * eps by ;
then A5: k < n * eps by ;
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 ; :: thesis: verum
end;
thus aseq k is convergent by A1; :: thesis: lim (aseq k) = 1
hence lim (aseq k) = 1 by ; :: thesis: verum