In [1]:

```
import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprTuple, ExprRange
from proveit import k, m, x, S
from proveit.core_expr_types import a_1_to_m, A_1_to_m
from proveit.logic import And, Forall, InSet, Equals, CartProd, CartExp
from proveit.logic.sets.cartesian_products import a_in_A__1_to_m
from proveit.numbers import NaturalPos, one
```

In [2]:

```
%begin axioms
```

A Cartesian product set is the set of tuples whose elements are contained in the respective sets of the product.

In [3]:

```
cart_prod_def = Forall(
m, Forall((x, A_1_to_m, a_1_to_m),
Equals(InSet(x, CartProd(A_1_to_m)),
And(Equals(x, ExprTuple(a_1_to_m)),
a_in_A__1_to_m)).with_wrap_after_operator()),
domain=NaturalPos)
```

A Cartesian exponentiation is the set defined by the Cartesian product of the base repeated the number of times indicated by the exponent.

In [4]:

```
cart_exp_def = Forall(
m, Forall(S,
Equals(CartExp(S, m),
CartProd(ExprRange(k, S, one, m)))),
domain=NaturalPos)
```

In [5]:

```
%end axioms
```