theorem Th16: :: HILBASIS:16

for L being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for x, y being Element of (Polynom-Ring L)
for p, q being sequence of L st x = p & y = q holds
x - y = p - q