theorem :: FVSUM_1:52

for K being non empty multMagma
for a, a1 being Element of K holds a * <*a1*> = <*(a * a1)*>