```
(def-quasi-constructor m-composition
"lambda(f:[ind_2,ind_3],g:[ind_1,ind_2], lambda(x:ind_1, f(g(x))))"
(language pure-generic-theory-3)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-domain
"lambda(f:[ind_1,ind_2], indic(x:ind_1, #(f(x))))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-range
"lambda(f:[ind_1,ind_2], indic(y:ind_2, forsome(x:ind_1, y=f(x))))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-image
"lambda(f:[ind_1,ind_2],a:sets[ind_1],
indic(y:ind_2, forsome(x:ind_1, (x in a) and y=f(x))))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-inverse-image
"lambda(f:[ind_1,ind_2],b:sets[ind_2], b oo f)"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-inverse
"lambda(f:[ind_1,ind_2],
lambda(x:ind_2, iota(y:ind_1, f(y)=x)))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-id
"lambda(a:sets[ind_1],
lambda(x:ind_1, if(x in a, x, ?ind_1)))"
(language pure-generic-theory-1)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-restrict
"lambda(f:[ind_1,ind_2],a:sets[ind_1],
lambda(x:ind_1, if(x in a, f(x), ?ind_2)))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-restrict2
"lambda(f:[ind_1,ind_2,ind_3],a:sets[ind_1],b:sets[ind_2],
lambda(x:ind_1,y:ind_2, if(x in a and y in b, f(x,y), ?ind_3)))"
(language pure-generic-theory-3)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-surjective?
"lambda(f:[ind_1,ind_2],
forall(x:ind_1, x in dom(f)) and forall(y:ind_2, y in ran(f)))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-injective?
"lambda(f:[ind_1,ind_2],
forall(x_1,x_2:ind_1, f(x_1)=f(x_2) implies x_1=x_2))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-bijective?
"lambda(f:[ind_1,ind_2], surjective_q(f) and injective_q(f))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-surjective-on?
"lambda(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
dom(f)=a and ran(f)=b)"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-injective-on?
"lambda(f:[ind_1,ind_2],a:sets[ind_1],
forall(x_1,x_2:ind_1,
((x_1 in a) and (x_2 in a) and f(x_1)=f(x_2)) implies x_1=x_2))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```

```
(def-quasi-constructor m-bijective-on?
"lambda(f:[ind_1,ind_2],a:sets[ind_1],b:sets[ind_2],
surjective_on_q(f,a,b) and injective_on_q(f,a))"
(language pure-generic-theory-2)
(fixed-theories the-kernel-theory))
```