:: deftheorem Def2 defines |. POLYNOM5:def 2 :
for p being complex-valued FinSequence
for b₂ being FinSequence of REAL holds
( b₂ = |.p.| iff ( len b₂ = len p & ( for n being Nat st n in dom p holds
b₂ . n = |.(p . n).| ) ) );