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_{1} being set holds

( not N <= b_{1} or not (seq_id (id NAT)) . b_{1} = 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

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

( not N <= b

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