let i be Nat; :: thesis: for a being Element of COMPLEX
for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt (R1,R2)) = mlt ((a * R1),R2)
let a be Element of COMPLEX ; :: thesis: for R1, R2 being Element of i -tuples_on COMPLEX holds a * (mlt (R1,R2)) = mlt ((a * R1),R2)
let R1, R2 be Element of i -tuples_on COMPLEX; :: thesis: a * (mlt (R1,R2)) = mlt ((a * R1),R2)
thus a * (mlt (R1,R2)) = (multcomplex [;] (a,(id COMPLEX))) * (mlt (R1,R2)) by Lm1
.= multcomplex .: (((multcomplex [;] (a,(id COMPLEX))) * R1),R2) by FINSEQOP:26
.= mlt ((a * R1),R2) by Lm1 ; :: thesis: verum