:: deftheorem Def5 defines delta_1 E_TRANS2:def 6 :
for m being positive Nat
for p being prime odd Nat
for g being non zero Polynomial of INT.Ring
for b₄ being FinSequence of F_Real holds
( b₄ = delta_1 (m,p,g) iff ( len b₄ = m & ( for i being Nat st i in dom b₄ holds
b₄ . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) ) ) );