theorem Th44: :: POLYNOM9:44
for X being set
for S being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for p being Series of X,S
for a being Element of S holds vars (a * p) c= vars p