let i, j be natural Number ; :: 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))
reconsider i = i, j = j as Nat by TARSKI:1;
Product ((i + j) |-> z) = multcomplex . ((multcomplex $$ (i |-> z)),(multcomplex $$ (j |-> z))) by SETWOP_2:26
.= (Product (i |-> z)) * (Product (j |-> z)) by BINOP_2:def 5 ;
hence Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z)) ; :: thesis: verum