background image

Proof.

X

[

g

f

]

Y , Y uh

g

f

iX

=

/ 0

F

(

Dst

g

)

, Y u h

g

ih

f

iX

=

/ 0

F

(

Dst

g

)

, h

f

iX

[

g

]

Y , X

([

g

]

h

f

i

)

Y

for every

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

g

)

.

[

g

f

]=[(

f

¡

1

g

¡

1

)

¡

1

]

,

[

f

¡

1

g

¡

1

]

¡

1

=([

f

¡

1

]

h

g

¡

1

i

)

¡

1

=

h

g

¡

1

i

¡

1

[

f

]

.

Corollary 6.43.

[

f

]=[

id

Dst

f

]

h

f

i

for every funcoid

f

.

The following theorem is a variant for funcoids of the statement (which denes compositions

of relations) that

x

(

g

f

)

z

, 9

y

: (

x f y

^

y g z

)

for every

x

and

z

and every binary relations

f

and

g

.

Theorem 6.44.

For every sets

A

,

B

,

C

and

f

2

FCD

(

A

;

B

)

,

g

2

FCD

(

B

;

C

)

and

X 2

F

(

A

)

,

Z 2

F

(

C

)

X

[

g

f

]

Z , 9

y

2

atoms

F

(

B

)

: (

X

[

f

]

y

^

y

[

g

]

Z

)

:

Proof.

9

y

2

atoms

F

(

B

)

: (

X

[

f

]

y

^

y

[

g

]

Z

)

,

9

y

2

atoms

F

(

B

)

:

¡

Z u h

g

i

y

=

/ 0

F

(

C

)

^

y

u h

f

iX

=

/ 0

F

(

B

)

,

9

y

2

atoms

F

(

B

)

:

¡

Z u h

g

i

y

=

/ 0

F

(

C

)

^

y

v h

f

iX

)

Z u h

g

ih

f

iX

=

/ 0

F

(

C

)

,

X

[

g

f

]

Z

:

Reversely, if

X

[

g

f

]

Z

then

h

f

iX

[

g

]

Z

, consequently there exists

y

2

atoms

h

f

iX

such that

y

[

g

]

Z

;

we have

X

[

f

]

y

.

Theorem 6.45.

For every sets

A

,

B

,

C

1.

f

(

g

t

h

) =

f

g

t

f

h

for

g; h

2

FCD

(

A

;

B

)

and

f

2

FCD

(

B

;

C

)

;

2.

(

g

t

h

)

f

=

g

f

t

h

f

for

g; h

2

FCD

(

B

;

C

)

and

f

2

FCD

(

A

;

B

)

.

Proof.

I will prove only the rst equality because the other is analogous.

For every

X 2

F

(

A

)

,

Z 2

F

(

C

)

X

[

f

(

g

t

h

)]

Z , 9

y

2

atoms

F

(

B

)

: (

X

[

g

t

h

]

y

^

y

[

f

]

Z

)

, 9

y

2

atoms

F

(

B

)

: ((

X

[

g

]

y

_ X

[

h

]

y

)

^

y

[

f

]

Z

)

, 9

y

2

atoms

F

(

B

)

: ((

X

[

g

]

y

^

y

[

f

]

Z

)

_

(

X

[

h

]

y

^

y

[

f

]

Z

))

, 9

y

2

atoms

F

(

B

)

: (

X

[

g

]

y

^

y

[

f

]

Z

)

_ 9

y

2

atoms

F

(

B

)

: (

X

[

h

]

y

^

y

[

f

]

Z

)

, X

[

f

g

]

Z _ X

[

f

h

]

Z

, X

[

f

g

t

f

h

]

Z

:

Remark 6.46.

The above theorem can be proved without atomic lters by the formula

h

f

(

g

t

h

)

iX

=

h

f

ih

g

t

h

iX

=

h

f

i

(

h

g

iX t h

h

iX

) =

h

f

ih

g

iX t h

f

ih

h

iX

=

h

f

g

iX t h

f

h

iX

=

h

f

g

t

f

h

iX

.

[TODO: This may be useful for a pointfree generalization. Preserve old proof for

history.]

6.6 Domain and range of a funcoid

Denition 6.47.

Let

A

be a set. The

identity funcoid

id

FCD

(

A

)

= (

A

;

A

;

id

F

(

A

)

;

id

F

(

A

)

)

.

Obvious 6.48.

The identity funcoid is a funcoid.

Denition 6.49.

Let

A

be a set,

A 2

F

(

A

)

. The

restricted identity funcoid

id

A

FCD

= (

A

;

A

;

A u

;

A u

)

:

102

Funcoids