Proof.

card

h

f

1

i{

y

}

>

1

is obvious. It remains to show that

y

[

f

1

]

a

y

[

f

1

]

b

a

=

b

for every

a

and

b

. Really, let

y

[

f

1

]

a

y

[

f

1

]

b

. Then

y

=

fa

and

y

=

fb

and thus

a

=

b

because

y

∈ h

f

i

(

{

x

X

0

dom

A

|

ρ

0

x

=

A

} \

ZC

0

)

and

f

|

{

x

X

0

dom

A

|

ρ

0

x

=

A

}\

ZC

0

is an injection.

Fix quasi-cartesian situations

S

A

,

S

B

,

S

C

and quasi-cartesian functions

f

:

S

A

S

B

and

g

:

S

A

S

C

such that dom

f

=

dom

g

. Let

A

is a small indexed family of forms.

[TODO: Check below

formulations (it is possible that I’ve done little errors confusing

A

,

B

, and

C

).]

For a small indexed family

A

of forms let:

ϕ

A

=

g

id

{

x

X

A

dom

A

|

ρ

A

x

=

A

}

f

1

.

Obvious 15.

ϕ

A

=

g

|

{

x

X

A

dom

A

|

ρ

A

x

=

A

}

f

1

=

g

f

|

{

x

X

A

dom

A

|

ρ

A

x

=

A

}

1

.

Proposition 16.

ϕ

A

is a function and

dom

ϕ

A

=

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

and for every

y

dom

ϕ

A

we have

ϕ

A

y

=

(

Z

C

g

A

)

if

y

=

Z

B

f

A

);

g f

1

y

if

y

Z

B

f

A

)

.

Proof.

It follows from the previous proposition.

Theorem 17.

ϕ

A

=

g

f

1

|

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

.

Proof.

If

y

(

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

)

\ {

Z

B

f

A

)

}

then card

h

f

1

i{

y

}

= 1

and thus

h

f

i{

y

} ∈ {

x

X

B

dom

A

|

ρ

B

x

=

A

} \

ZC

B

. Consequently

h

ϕ

A

i{

y

}

=

h

g

f

1

i{

y

}

=

g

f

1

|

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

{

y

}

.

h

ϕ

A

i{

Z

B

f

A

)

}

=

Z

C

g

A

)

and

g

f

1

|

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

{

Z

C

g

A

)

}

=

h

g

f

1

i{

Z

C

g

A

)

}

=

h

g

i

(

{

x

X

A

dom

A

|

ρ

A

x

=

A

} ∩

ZC

A

) =

Z

C

g

A

)

.

Thus

h

ϕ

A

i{

y

}

=

g

f

1

|

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

{

y

}

for every

y

∈ h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

.

Theorem 18.

ϕ

A

is a bijection

h

f

i{

x

X

A

dom

A

|

ρ

A

x

=

A

} → h

g

i{

x

X

A

dom

A

|

ρ

A

x

=

A

}

.

Proof.

That

ϕ

A

is a surjection

h

f

i{

x

X

A

dom

A

|

ρ

0

x

=

A

} → h

g

i{

x

X

A

dom

A

|

ρ

0

x

=

A

}

follows from a proposition above and symmetry. To prove that it is an injection is enough to show
that:

1.

g f

1

y

Z

C

g

A

)

if

y

Z

B

f

A

)

for every

y

dom

ϕ

A

.

3