let i be Element of 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:27, GROUP_1:31; :: thesis: a * (mlt R1,R2) = mlt R1,(a * R2)
thus a * (mlt R1,R2) = a * (mlt R2,R1) by FINSEQOP:34
.= mlt (a * R2),R1 by FINSEQOP:27, GROUP_1:31
.= mlt R1,(a * R2) by FINSEQOP:34 ; :: thesis: verum