theorem Th33a: :: POLYNOM3:36

for L being non empty right_complementable add-associative right_zeroed left-distributive well-unital doubleLoopStr
for p being sequence of L holds (1_. L) *' p = p