let a be non negative Real; :: thesis: for n being Nat st 1 <= n holds
0 < (seq_n^ a) . n
let n be Nat; :: thesis: ( 1 <= n implies 0 < (seq_n^ a) . n )
AA: n in NAT by ORDINAL1:def 12;
assume AS: 1 <= n ; :: thesis: 0 < (seq_n^ a) . n
then (seq_n^ a) . n = n to_power a by AA, ASYMPT_1:def 3;
hence 0 < (seq_n^ a) . n by AS, POWER:34; :: thesis: verum