theorem :: FVSUM_1:69

for i being Nat
for K being non empty associative commutative multMagma
for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds
( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )