theorem :: FVSUM_1:63

for i being Nat
for K being non empty commutative multMagma
for R1, R2 being Element of i -tuples_on the carrier of K holds mlt (R1,R2) = mlt (R2,R1) by FINSEQOP:33;