let k be Element of NAT ; :: thesis: ( aseq k is convergent & lim (aseq k) = 1 )
A1: for eps being real number st 0 < eps holds
ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs (((aseq k) . n) - 1) < eps

proof

let eps be real number ; :: thesis: ( 0 < eps implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs (((aseq k) . n) - 1) < eps )
assume A2: eps > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs (((aseq k) . n) - 1) < eps
consider N being Element of NAT such that
A3: N > k / eps by SEQ_4:10;
take N ; :: thesis: for n being Element of NAT st N <= n holds
abs (((aseq k) . n) - 1) < eps
let n be Element of NAT ; :: thesis: ( N <= n implies abs (((aseq k) . n) - 1) < eps )
assume A5: n >= N ; :: thesis: abs (((aseq k) . n) - 1) < eps
then A6: n > 0 by A2, A3;
then A7: abs (((aseq k) . n) - 1) = abs ((1 - (k / n)) - 1) by Th8
.= abs (- (k / n))
.= abs (k / n) by COMPLEX1:138
.= k / n by ABSVALUE:def 1 ;
n > k / eps by A3, A5, XXREAL_0:2;
then (k / eps) * eps < n * eps by A2, XREAL_1:70;
then k < n * eps by A2, XCMPLX_1:88;
hence abs (((aseq k) . n) - 1) < eps by A6, A7, XREAL_1:85; :: thesis: verum

end;

thus aseq k is convergent :: thesis: lim (aseq k) = 1

proof

take 1 ; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs K72(((aseq k) . b₃),1) ) )
thus for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs K72(((aseq k) . b₃),1) ) ) by A1; :: thesis: verum

end;

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