set f = seq_const 0;
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
|.((seq_const 0) . x).| < 1 / ((polynom c) . x)
take N = 0 ; :: thesis: for x being Nat st N <= x holds
|.((seq_const 0) . x).| < 1 / ((polynom c) . x)
let x be Nat; :: thesis: ( N <= x implies |.((seq_const 0) . x).| < 1 / ((polynom c) . x) )
D2: |.((seq_const 0) . x).| = |.0.| by SEQ_1:57
.= 0 ;
0 < (polynom c) . x by NLM3;
hence ( N <= x implies |.((seq_const 0) . x).| < 1 / ((polynom c) . x) ) by D2; :: thesis: verum