:: deftheorem Def6 defines delta_2 E_TRANS2:def 7 :
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
for b₅ being FinSequence of F_Real holds
( b₅ = delta_2 (m,p,g,z0) iff ( len b₅ = m & ( for i being Nat st i in dom b₅ holds
b₅ . i = - ((g . i) * (((power F_Real) . (z0,i)) * (('F' (f_0 (m,p))) . 0))) ) ) );