let k, n be Nat; ( 0 < n implies n * ((seq_n^ k) . n) = (seq_n^ (k + 1)) . n )
ZZ:
( k in NAT & n in NAT )
by ORDINAL1:def 12;
assume AS:
0 < n
; n * ((seq_n^ k) . n) = (seq_n^ (k + 1)) . n
(seq_n^ (k + 1)) . n =
n to_power (k + 1)
by ZZ, ASYMPT_1:def 3, AS
.=
(n to_power k) * (n to_power 1)
by POWER:27, AS
.=
(n to_power k) * n
by POWER:25
;
hence
n * ((seq_n^ k) . n) = (seq_n^ (k + 1)) . n
by AS, ZZ, ASYMPT_1:def 3; verum