let i be Nat; :: thesis: for R1, R2 being i -element complex-valued FinSequence holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)
let R1, R2 be i -element complex-valued FinSequence; :: thesis: Product (mlt (R1,R2)) = (Product R1) * (Product R2)
reconsider R1 = R1, R2 = R2 as i -element FinSequence of COMPLEX by FINSEQ_1:102;
reconsider T1 = R1, T2 = R2 as Element of i -tuples_on COMPLEX by FINSEQ_2:131;
Product (mlt (R1,R2)) = multcomplex . ((multcomplex $$ T1),(multcomplex $$ T2)) by SETWOP_2:35
.= (Product R1) * (Product R2) by BINOP_2:def 5 ;
hence Product (mlt (R1,R2)) = (Product R1) * (Product R2) ; :: thesis: verum