theorem TPOWSUCC: :: ASYMPT_2:37

for k, n being Nat st 0 < n holds
n * ((seq_n^ k) . n) = (seq_n^ (k + 1)) . n