theorem Th10: :: E_TRANS2:10

for k being non zero Nat
for p being prime odd Nat holds
( (x. (k,p)) ^ <*((tau (k + 1)) |^ p)*> = x. ((k + 1),p) & Product (x. ((k + 1),p)) = (Product (x. (k,p))) * ((tau (k + 1)) |^ p) )