:: deftheorem defines * FVSUM_1:def 6 :
for K being non empty multMagma
for p being FinSequence of the carrier of K
for a being Element of K holds a * p = (a multfield) * p;