theorem Th37: :: E_TRANS2:34

for p being prime odd Nat
for m being positive Nat
for g being non zero Polynomial of INT.Ring st deg g = m holds
for x being non zero Element of F_Real holds Sum (delta_2 (m,p,g,x)) = ((g . 0) * (('F' (f_0 (m,p))) . 0)) - ((Ext_eval (g,x)) * (('F' (f_0 (m,p))) . 0))