set f = seq_id (id NAT);
A0: dom (id NAT) = NAT ;
rng (id NAT) c= REAL ;
then A1: id NAT is Function of NAT,REAL by A0, FUNCT_2:2;
take N = 1; :: according to ASYMPT_0:def 5 :: thesis: for b₁ being set holds
( not N <= b₁ or not (seq_id (id NAT)) . b₁ = 0 )
let n be Nat; :: thesis: ( not N <= n or not (seq_id (id NAT)) . n = 0 )
assume n >= N ; :: thesis: not (seq_id (id NAT)) . n = 0
hence not (seq_id (id NAT)) . n = 0 by FUNCT_1:18, A1, ORDINAL1:def 12; :: thesis: verum