 9.5. COMPLETE FUNCOIDS AND RELOIDS

211

F

(

B

)

A

ComplFCD

(

A, B

)

ComplRLD

(

A, B

)

G

7→

d

n

{

α

RLD

G

(

α

)

α

A

o

G

7→

d

n

{

α

FCD

G

(

α

)

α

A

o

f

7→

(

α

7→h

f

i

{

α

}

)

(

RLD

)

out

(

FCD

)

Figure 8

It remains to apply lemma

196

(taking into account that

θ

can be decomposed

into

G

7→

d

n

{

α

RLD

G

(

α

)

α

A

o

1

and

G

7→

d

n

{

α

FCD

G

(

α

)

α

A

o

).

Theorem

1127

.

Composition of complete reloids is complete.

Proof.

Let

f

,

g

be complete reloids. Then (

FCD

)(

g

f

) = (

FCD

)

g

(

FCD

)

f

.

Thus (because (

FCD

)(

g

f

) is a complete funcoid) we have

g

f

= (

RLD

)

out

((

FCD

)

g

(

FCD

)

f

), but (

FCD

)

g

(

FCD

)

f

is a complete funcoid, thus

g

f

is a complete

reloid.

Theorem

1128

.

1

. (

RLD

)

out

g

(

RLD

)

out

f

= (

RLD

)

out

(

g

f

) for composable complete funcoids

f

and

g

.

2

. (

RLD

)

out

g

(

RLD

)

out

f

= (

RLD

)

out

(

g

f

) for composable co-complete fun-

coids

f

and

g

.

Proof.

Let

f

,

g

be composable complete funcoids.

(

FCD

)((

RLD

)

out

g

(

RLD

)

out

f

) = (

FCD

)(

RLD

)

out

g

(

FCD

)(

RLD

)

out

f

=

g

f

.

Thus (taking into account that (

RLD

)

out

g

(

RLD

)

out

f

is complete) we have

(

RLD

)

out

g

(

RLD

)

out

f

= (

RLD

)

out

(

g

f

).

For co-complete funcoids it’s dual.

Proposition

1129

.

If

f

is a (co-)complete funcoid then up

f

is a filter.

Proof.

It is enough to consider the case if

f

is complete.

We need to prove that

F, G

up

f

:

F

u

G

up

f

.

For every

F

Rel

(Src

f,

Dst

f

) we have

F

up

f

F

w

f

⇔ h

F

i

{

x

} w h

f

i

{

x

}

.

Thus

F, G

up

f

⇒ h

F

i

{

x

} w h

f

i

{

x

}∧h

G

i

{

x

} w h

f

i

{

x

} ⇒ h

F

u

G

i

{

x

}

=

h

F

i

{

x

} u h

G

i

{

x

} w h

f

i

{

x

} ⇒

F

u

G

up

f

.

That up

f

is nonempty and up-directed is obvious.

Corollary

1130

.

1

. If

f

is a (co-)complete funcoid then up

f

= up(

RLD

)

out

f

.