let a be Real; :: thesis: ( 1 <= a implies seq_a^ (a,1,0) is non-decreasing )
assume AS: 1 <= a ; :: thesis: seq_a^ (a,1,0) is non-decreasing
for n being Nat holds (seq_a^ (a,1,0)) . n <= (seq_a^ (a,1,0)) . (n + 1)

proof

let n be Nat; :: thesis: (seq_a^ (a,1,0)) . n <= (seq_a^ (a,1,0)) . (n + 1)
L2: (seq_a^ (a,1,0)) . n = a to_power ((1 * n) + 0) by ASYMPT_1:def 1
.= a to_power n ;
(seq_a^ (a,1,0)) . (n + 1) = a to_power ((1 * (n + 1)) + 0) by ASYMPT_1:def 1
.= a to_power (n + 1) ;
hence (seq_a^ (a,1,0)) . n <= (seq_a^ (a,1,0)) . (n + 1) by L2, LC5a, AS; :: thesis: verum

end;

hence seq_a^ (a,1,0) is non-decreasing by SEQM_3:def 8; :: thesis: verum