theorem Th27: :: POLYNOM3:29

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being sequence of L holds p - p = 0_. L