theorem Th46: :: POLYNOM9:46

for x being object
for X being Ordinal
for S being non trivial right_complementable add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of X,S
for t being bag of X holds vars (Subst (t,x,p)) c= ((support t) \ {x}) \/ (vars p)