let i, j be natural Number ; :: thesis: for z being Element of COMPLEX holds Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z)))
let z be Element of COMPLEX ; :: thesis: Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z)))
( i is Nat & j is Nat ) by TARSKI:1;
hence Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z))) by SETWOP_2:27; :: thesis: verum