let i be Nat; :: thesis: for R1, R2 being i -long FinSequence of COMPLEX holds Product (mlt R1,R2) = (Product R1) * (Product R2)
let R1, R2 be i -long FinSequence of COMPLEX ; :: thesis: Product (mlt R1,R2) = (Product R1) * (Product R2)
reconsider T1 = R1, T2 = R2 as Element of i -tuples_on COMPLEX by FINSEQ_2:151;
thus Product (mlt R1,R2) = multcomplex . (multcomplex $$ T1),(multcomplex $$ T2) by SETWOP_2:46
.= (Product R1) * (Product R2) by BINOP_2:def 5 ; :: thesis: verum