theorem :: NAT_1:50

for k being Nat
for X being non empty set
for s being sequence of X
for N being sequence of NAT holds (s * N) ^\ k = s * (N ^\ k)