theorem Th81: :: POLYNOM9:81

for X being set
for S being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Series of X,S
for V being set st vars p c= V & vars q c= V holds
vars (p - q) c= V