:: deftheorem defines multfield FVSUM_1:def 1 :
for K being non empty multMagma
for a being Element of K holds a multfield = the multF of K [;] (a,(id the carrier of K));