:: deftheorem Def4 defines Subst POLYNOM9:def 4 :
for X being Ordinal
for L being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p, s being Polynomial of X,L
for x being object
for b₆ being Polynomial of X,L holds
( b₆ = Subst (p,x,s) iff ex S being FinSequence of (Polynom-Ring (X,L)) st
( b₆ = Sum S & len (SgmX ((BagOrder X),(Support p))) = len S & ( for i being Nat st i in dom S holds
S . i = (p . ((SgmX ((BagOrder X),(Support p))) /. i)) * (Subst (((SgmX ((BagOrder X),(Support p))) /. i),x,s)) ) ) );