theorem Th64: :: FVSUM_1:64

for K being non empty commutative multMagma
for p, q being FinSequence of the carrier of K holds mlt (p,q) = mlt (q,p)