take 1 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not (seq_n^ a) . b₁ <= 0 )
set f = seq_n^ a;
let n be Element of NAT ; :: thesis: ( not 1 <= n or not (seq_n^ a) . n <= 0 )
assume A1: n >= 1 ; :: thesis: not (seq_n^ a) . n <= 0
then (seq_n^ a) . n = n to_power a by Def3;
hence not (seq_n^ a) . n <= 0 by A1, POWER:34; :: thesis: verum