theorem poly1: :: RING_4:12

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