:: deftheorem Def2 defines x. E_TRANS2:def 3 :
for p being non zero Nat
for m being Nat
for b₃ being FinSequence of the carrier of (Polynom-Ring INT.Ring) holds
( b₃ = x. (m,p) iff ( len b₃ = m & ( for i being Nat st i in dom b₃ holds
b₃ . i = (tau i) |^ p ) ) );