theorem Th27: :: POLYNOM5:27

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