let f be Function of NAT,REAL; :: thesis: ( f is negligible implies ( f is convergent & lim f = 0 ) )
assume AS: f is negligible ; :: thesis: ( f is convergent & lim f = 0 )
A1: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((f . m) - 0).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((f . m) - 0).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((f . m) - 0).| < p
then consider N being Nat such that
P1: for x being Nat st N <= x holds
|.(f . x).| < p by AS, PXR2;
reconsider N = N as Nat ;
take N ; :: thesis: for m being Nat st N <= m holds
|.((f . m) - 0).| < p
let m be Nat; :: thesis: ( N <= m implies |.((f . m) - 0).| < p )
assume P2: N <= m ; :: thesis: |.((f . m) - 0).| < p
reconsider x = m as Element of NAT by ORDINAL1:def 12;
thus |.((f . m) - 0).| < p by P1, P2; :: thesis: verum

end;

hence f is convergent by SEQ_2:def 6; :: thesis: lim f = 0
hence lim f = 0 by A1, SEQ_2:def 7; :: thesis: verum