theorem Th16: :: E_TRANS2:15

for p being prime odd Nat
for m being positive Nat holds
( len (x. (m,p)) = m & len (ff_0 (m,p)) = m + 1 & (ff_0 (m,p)) . ((len (x. (m,p))) + 1) = (tau 0) |^ (p -' 1) )