theorem :: FVSUM_1:62

for K being non empty multMagma
for a1, a2 being Element of K holds mlt (<*a1*>,<*a2*>) = <*(a1 * a2)*> by FINSEQ_2:74;