theorem Th22: :: UPROOTS:25

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