:: deftheorem Def6 defines Subst POLYNOM5:def 6 :
for L being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr
for p, q, b₄ being Polynomial of L holds
( b₄ = Subst (p,q) iff ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b₄ = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) );