:: deftheorem defines delta E_TRANS2:def 8 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring
for z0 being non zero Element of F_Real holds delta (m,p,g,z0) = (delta_1 (m,p,g)) + (delta_2 (m,p,g,z0));