for K being non empty multMagma
for a, b being Element of K holds (a multfield) . b = a * b by Th48;