theorem Th66: :: FVSUM_1:66

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