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:27
.= mlt (a * R1),R2 by Lm1 ; :: thesis: verum