:: deftheorem Def9 defines |. E_TRANS2:def 1 :
for p being Polynomial of INT.Ring
for b₂ being sequence of INT.Ring holds
( b₂ = |.p.| iff for n being Nat holds b₂ . n = |.(p . n).| );