theorem poly2a: :: RING_4:9

for L being non empty left_unital doubleLoopStr
for p being sequence of L holds (1. L) * p = p