theorem Th9: :: POLYALG1:9

for L being non empty well-unital associative doubleLoopStr
for p being sequence of L holds (1. L) * p = p