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

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