theorem Th79: :: POLYNOM9:79

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
for V being set st vars p c= V & vars q c= V holds
vars (p *' q) c= V