let f be Function of NAT,REAL; :: thesis: ( f is negligible implies for r being Real st 0 < r holds
ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < r )
assume AS: f is negligible ; :: thesis: for r being Real st 0 < r holds
ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < r
let r be Real; :: thesis: ( 0 < r implies ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < r )
assume 0 < r ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < r
then consider c being non empty positive-yielding XFinSequence of REAL such that
P1: for x being Nat holds (polynom c) . x = 1 / r by PXR1;
consider N being Nat such that
P2: for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x) by AS;
take N ; :: thesis: for x being Nat st N <= x holds
|.(f . x).| < r
thus for x being Nat st N <= x holds
|.(f . x).| < r :: thesis: verum

proof

let x be Nat; :: thesis: ( N <= x implies |.(f . x).| < r )
assume N <= x ; :: thesis: |.(f . x).| < r
then |.(f . x).| < 1 / ((polynom c) . x) by P2;
then |.(f . x).| < 1 / (1 / r) by P1;
hence |.(f . x).| < r by XCMPLX_1:52; :: thesis: verum

end;