cartesian_product_n the cartesian product of n copies of the first argument. Binary function. $ Z^m \times Z^n = Z^{m+n} $ (set1p.cartesian_product_n(setname1.Z, m) ~set1.cartesian_product~ set1p.cartesian_product_n(setname1.Z, n)) ~relation1.eq~ set1p.cartesian_product_n(setname1.Z, arith1.plus(m,n));