let a be positive Real; :: thesis: seq_a^ (a,1,0) is positive

now :: thesis: for n being Nat holds 0 < (seq_a^ (a,1,0)) . n

hence
seq_a^ (a,1,0) is positive
; :: thesis: verumlet n be Nat; :: thesis: 0 < (seq_a^ (a,1,0)) . n

(seq_a^ (a,1,0)) . n = a to_power ((1 * n) + 0) by ASYMPT_1:def 1

.= a to_power n ;

hence 0 < (seq_a^ (a,1,0)) . n by POWER:34; :: thesis: verum

end;(seq_a^ (a,1,0)) . n = a to_power ((1 * n) + 0) by ASYMPT_1:def 1

.= a to_power n ;

hence 0 < (seq_a^ (a,1,0)) . n by POWER:34; :: thesis: verum