theorem :: FVSUM_1:65
for i being Nat
for K being non empty associative multMagma
for R1, R2, R3 being Element of i -tuples_on the carrier of K holds mlt (R1,(mlt (R2,R3))) = mlt ((mlt (R1,R2)),R3) by FINSEQOP:28;