:: deftheorem defines ^delta E_TRANS2:def 9 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring holds ^delta (m,p,g) = delta_1 (m,p,g);