:: deftheorem defines ff_0 E_TRANS2:def 4 :
for p being prime odd Nat
for m being positive Nat holds ff_0 (m,p) = (x. (m,p)) ^ <*((tau 0) |^ (p -' 1))*>;