:: deftheorem Def2 defines |. POLYNOM5:def 2 :
for p being FinSequence of the carrier of F_Complex
for b₂ being FinSequence of REAL holds
( b₂ = |.p.| iff ( len b₂ = len p & ( for n being Element of NAT st n in dom p holds
b₂ /. n = |.(p /. n).| ) ) );