set f = seq_n! a;
take 0 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 0 <= b₁ or not (seq_n! a) . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 0 <= n or not (seq_n! a) . n <= 0 )
assume n >= 0 ; :: thesis: not (seq_n! a) . n <= 0
(seq_n! a) . n = (n + a) ! by Def5;
hence not (seq_n! a) . n <= 0 by NEWTON:23; :: thesis: verum