let i be Nat; :: thesis: 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)) )
let K be non empty associative commutative multMagma ; :: thesis: 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)) )
let a be Element of K; :: thesis: 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)) )
let R1, R2 be Element of i -tuples_on the carrier of K; :: thesis: ( a * (mlt (R1,R2)) = mlt ((a * R1),R2) & a * (mlt (R1,R2)) = mlt (R1,(a * R2)) )
thus a * (mlt (R1,R2)) = mlt ((a * R1),R2) by FINSEQOP:26; :: thesis: a * (mlt (R1,R2)) = mlt (R1,(a * R2))
thus a * (mlt (R1,R2)) = a * (mlt (R2,R1)) by FINSEQOP:33
.= mlt ((a * R2),R1) by FINSEQOP:26
.= mlt (R1,(a * R2)) by FINSEQOP:33 ; :: thesis: verum