let cF1, cF2 be complex-valued XFinSequence; :: thesis: Product (cF1 ^ cF2) = (Product cF1) * (Product cF2)
thus Product (cF1 ^ cF2) = multcomplex . ((Product cF1),(Product cF2)) by AFINSQ_2:42
.= (Product cF1) * (Product cF2) by BINOP_2:def 5 ; :: thesis: verum