:: deftheorem Def3 defines Subst POLYNOM9:def 3 :
for X being Ordinal
for L being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for t being bag of X
for p being Polynomial of X,L
for x being object
for b₆ being Series of X,L holds
( b₆ = Subst (t,x,p) iff for b being bag of X holds
( ( ex s being bag of X st b = Subst (t,x,s) implies for s being bag of X st b = Subst (t,x,s) holds
b₆ . b = (p `^ (t . x)) . s ) & ( ( for s being bag of X holds b <> Subst (t,x,s) ) implies b₆ . b = 0. L ) ) );