let a be Real; ( 1 <= a implies seq_a^ (a,1,0) is V51() )
assume AS:
1 <= a
; seq_a^ (a,1,0) is V51()
for n being Nat holds (seq_a^ (a,1,0)) . n <= (seq_a^ (a,1,0)) . (n + 1)
proof
let n be
Nat;
(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;
verum
end;
hence
seq_a^ (a,1,0) is V51()
by SEQM_3:def 8; verum