take 0 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set holds
( not 0 <= b₁ or not (seq_a^ (a,b,c)) . b₁ <= 0 )
set f = seq_a^ (a,b,c);
let n be Nat; :: thesis: ( not 0 <= n or not (seq_a^ (a,b,c)) . n <= 0 )
A1: n in NAT by ORDINAL1:def 12;
assume n >= 0 ; :: thesis: not (seq_a^ (a,b,c)) . n <= 0
(seq_a^ (a,b,c)) . n = a to_power ((b * n) + c) by Def1, A1;
hence not (seq_a^ (a,b,c)) . n <= 0 by POWER:34; :: thesis: verum