theorem Th43: :: POLYNOM9:43

for X being Ordinal
for S being non empty right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p, q being Polynomial of X,S holds vars (p *' q) c= (vars p) \/ (vars q)