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 Function, Lambda, Conditional, Composition
from proveit import i, a, b, c, f, g, m, x, y, z, B, Q, fx, fy, gy, gz
from proveit.core_expr_types import (
a_1_to_i, b_1_to_i, c_1_to_i,
f__a_1_to_i, g__a_1_to_i, f__b_1_to_i, g__c_1_to_i,
A_1_to_m)
#from proveit.core_expr_types.tuples import f_x
from proveit.logic import Implies, Forall, Equals
from proveit.numbers import NaturalPos
```

In [2]:

```
%begin axioms
```

**A Lambda map is as a Lambda map does. Thus, Lambda maps are defined to be equal if they preform the same transformation under the pertinent conditions. This is similar to the proveit.logic.equality.substitution axiom except that the substitution is performed within a Lambda map which requires a special rule due to scoping restriction.**

In [3]:

```
lambda_substitution = \
Forall(i, Forall((f, g),
Implies(Forall(a_1_to_i,
Equals(f__a_1_to_i,
g__a_1_to_i)),
Equals(Lambda(b_1_to_i, f__b_1_to_i),
Lambda(c_1_to_i, g__c_1_to_i)) \
.with_wrap_after_operator()).with_wrap_after_operator()),
domain=NaturalPos)
```

*The unary composition of a single map is just that map.*

In [4]:

```
unary_composition = \
Forall((f, g), Equals(Composition(Lambda(x, fx)),
Lambda(y, fy)))
```

*Define a binary composition.*

In [5]:

```
binary_composition = \
Forall((f, g), Equals(Composition(Lambda(x, fx), Lambda(y, gy)),
Lambda(z, Function(f, gz))))
```

*Define an n-ary composition.*

In [6]:

```
multi_composition_def = \
Forall(m, Forall((A_1_to_m, B),
Equals(Composition(A_1_to_m, B),
Composition(Composition(A_1_to_m), B)).with_wrap_after_operator()),
domain=NaturalPos)
```

In [7]:

```
%end axioms
```