theorem Th5: :: POLYALG1:5

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