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

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

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

thus
aseq k is convergent
by A1; :: thesis: lim (aseq k) = 1
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;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

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