theorem Th12: :: E_TRANS2:12

for p being prime odd Nat
for m being positive Nat holds len (~ (f_0 (m,p))) = (m * p) + p