theorem Th45: :: POLYNOM9:45

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 k being Nat holds vars (p `^ k) c= vars p