theorem Th7: :: POLYNOM1:7

for L being non empty multMagma
for a being Element of L holds (<*> the carrier of L) * a = <*> the carrier of L