background image

19.17. BINARY RELATIONS ARE POINTFREE FUNCOIDS

311

Proof.

Because it is a functor which preserves reversal.

Proposition

1610

.

The bijection defined by theorem

1606

preserves domain

an image.

Proof.

im

f

=

h

f

i>

=

h

p

i

>

= im

p

, likewise for domain.

Proposition

1611

.

The bijection defined by theorem

1606

maps cartesian

products to corresponding funcoidal products.

Proof.

A

×

FCD

B

X

=

(

B

if

X

6

A

if

X

A

=

h

A

×

B

i

X

.

Likewise

(

A

×

FCD

B

)

1

Y

=

(

A

×

B

)

1

Y

.

»»»> master