theorem Th20: :: E_TRANS2:17

for p being prime odd Nat
for m being positive Nat holds (~ (Product (x. (m,p)))) . 0 = (((- 1) |^ m) * (m !)) |^ p