let i, j be natural Number ; :: thesis: for r being Real holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
let r be Real; :: thesis: Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))
reconsider r = r as Element of REAL by XREAL_0:def 1;
reconsider pr = Product (i |-> r) as Element of REAL ;
( i is Nat & j is Nat ) by TARSKI:1;
then Product ((i * j) |-> r) = Product (j |-> pr) by SETWOP_2:27;
hence Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r))) ; :: thesis: verum