:: deftheorem Def7 defines ^ E_TRANS1:def 6 :
for F being FinSequence of the carrier of (Polynom-Ring INT.Ring)
for b₂ being FinSequence of the carrier of (Polynom-Ring F_Real) holds
( b₂ = ^ F iff ( dom b₂ = dom F & ( for i being Nat st i in dom F holds
b₂ . i = ^ (F /. i) ) ) );