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