theorem Th80: :: POLYNOM9:80

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