theorem Th11: :: E_TRANS2:11

for p being prime odd Nat
for m being positive Nat holds len (~ (Product (x. (m,p)))) = (m * p) + 1