let i, j be Nat; :: thesis: for c being Complex holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))
let c be Complex; :: thesis: Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))
reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;
Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c))) by SETWOP_2:27;
hence Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c))) ; :: thesis: verum