theorem Th49: :: NUMBER15:49

for s being Nat
for k, w being non zero Nat st k <= s & w <= s & w <> k holds
((idseq s) to_power (sequenceA s)) . w = (((idseq s) to_power (sequenceAnPk (s,k))) |^ (primenumber (k - 1))) . w