for K being non empty multMagma
for a, b being Element of K holds ( the multF of K [;] (a,(id the carrier of K))) . b = a * b