let i, j be Nat; :: thesis: for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))
let z be Element of COMPLEX ; :: thesis: Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))
thus Product ((i + j) |-> z) = multcomplex . ((multcomplex $$ (i |-> z)),(multcomplex $$ (j |-> z))) by SETWOP_2:37
.= (Product (i |-> z)) * (Product (j |-> z)) by BINOP_2:def 5 ; :: thesis: verum