let i, j be Nat; :: thesis: for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
let r be real number ; :: thesis: Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
reconsider r = r as Element of REAL by XREAL_0:def 1;
Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) by SETWOP_2:27;
hence Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) ; :: thesis: verum