take
0
; ASYMPT_0:def 4 for b1 being set holds
( not 0 <= b1 or not (seq_a^ (a,b,c)) . b1 <= 0 )
set f = seq_a^ (a,b,c);
let n be Nat; ( not 0 <= n or not (seq_a^ (a,b,c)) . n <= 0 )
A1:
n in NAT
by ORDINAL1:def 12;
assume
n >= 0
; 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; verum