:: deftheorem defines f_0 E_TRANS2:def 5 :
for p being prime odd Nat
for m being positive Nat holds f_0 (m,p) = Product (ff_0 (m,p));