theorem Th6: :: POLYNOM1:6

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