theorem Th47: :: POLYNOM9:47

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, s being Polynomial of X,S holds vars (Subst (p,x,s)) c= ((vars p) \ {x}) \/ (vars s)