let f be Function of NAT,REAL; :: thesis: ( ( for x being Nat holds f . x = 1 / (2 to_power x) ) implies f is negligible )
assume AS: for x being Nat holds f . x = 1 / (2 to_power x) ; :: thesis: f is negligible
let c be non empty positive-yielding XFinSequence of REAL ; :: according to ASYMPT_3:def 4 :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x)
set k = len c;
deffunc H₁( Nat) -> Element of omega = 1 * ($1 to_power (len c));
consider y being Real_Sequence such that
P1: for x being Nat holds y . x = H₁(x) from SEQ_1:sch 1();
consider N1 being Nat such that
P2: for x being Nat st N1 <= x holds
|.((seq_p c) . x).| <= y . x by ASYMPT_2:43, P1;
consider N2 being Nat such that
P3: for x being Nat st N2 <= x holds
1 / (2 to_power x) < 1 / (x to_power (len c)) by L2;
set N = N1 + N2;
reconsider N = N1 + N2 as Element of NAT by ORDINAL1:def 12;
take N ; :: thesis: for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x)
thus for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x) :: thesis: verum

proof

let x be Nat; :: thesis: ( N <= x implies |.(f . x).| < 1 / ((polynom c) . x) )
assume D3: N <= x ; :: thesis: |.(f . x).| < 1 / ((polynom c) . x)
K1: f . x = 1 / (2 to_power x) by AS;
N2 <= N by NAT_1:12;
then N2 <= x by D3, XXREAL_0:2;
then 1 / (2 to_power x) < 1 / (x to_power (len c)) by P3;
then P4: |.(f . x).| < 1 / (x to_power (len c)) by K1, ABSVALUE:def 1;
N1 <= N by NAT_1:12;
then N1 <= x by D3, XXREAL_0:2;
then |.((polynom c) . x).| <= y . x by P2;
then (polynom c) . x <= y . x by ABSVALUE:def 1;
then (polynom c) . x <= 1 * (x to_power (len c)) by P1;
then 1 / (x to_power (len c)) <= 1 / ((polynom c) . x) by XREAL_1:118, NLM3;
hence |.(f . x).| < 1 / ((polynom c) . x) by P4, XXREAL_0:2; :: thesis: verum

end;