background image

9.5. COMPLETE FUNCOIDS AND RELOIDS

209

Let

F

atoms(

RLD

)

in

f

,

G

atoms(

RLD

)

in

g

. Then dom

F

×

FCD

im

F

v

f

and

dom

G

×

FCD

im

G

v

g

. Provided that im

F

6

dom

G

, we have:

dom

F

×

RLD

im

G

= (dom

G

×

RLD

im

G

)

(dom

F

×

RLD

im

F

) =

RLD

l

G

0

F

0

F

0

atoms(dom

F

×

RLD

im

F

)

, G

0

atoms(dom

G

×

RLD

im

G

)

v

(*)

RLD

l

G

0

F

0

F

0

atoms

RLD

(Src

F,

Dst

F

)

, G

0

atoms

RLD

(Src

G,

Dst

G

)

, F

0

v

(

RLD

)

in

f, G

0

v

(

RLD

)

in

g

=

RLD

l

G

0

F

0

F

0

atoms(

RLD

)

in

f, G

0

atoms(

RLD

)

in

g

= (

RLD

)

in

g

(

RLD

)

in

f.

(*)

F

0

atoms(dom

F

×

RLD

im

F

) and dom

F

×

FCD

im

F

v

f

implies dom

F

0

×

FCD

im

F

0

v

f

; thus dom

F

0

×

RLD

im

F

0

v

(

RLD

)

in

f

and thus

F

0

v

(

RLD

)

in

f

. Likewise

for

G

and

G

0

.

Thus (

RLD

)

in

g

(

RLD

)

in

f

w

d

RLD

n

dom

F

×

RLD

im

G

F

atoms(

RLD

)

in

f,G

atoms(

RLD

)

in

g,

im

F

6

dom

G

o

.

But (

RLD

)

in

g

(

RLD

)

in

f

v

d

RLD

n

(dom

G

×

RLD

im

G

)

(dom

F

×

RLD

im

F

)

F

atoms(

RLD

)

in

f,G

atoms(

RLD

)

in

g

o

=

d

RLD

n

dom

F

×

RLD

im

G

F

atoms(

RLD

)

in

f,G

atoms(

RLD

)

in

g,

im

F

6

dom

G

o

.

Thus

(

RLD

)

in

g

(

RLD

)

in

f

=

RLD

l

dom

F

×

RLD

im

G

F

atoms(

RLD

)

in

f, G

atoms(

RLD

)

in

g,

im

F

6

dom

G

=

RLD

l

dom

F

×

RLD

im

G

F

atoms

RLD

(Src

f,

Dst

f

)

, G

atoms

RLD

(Dst

f,

Dst

g

)

,

dom

F

×

FCD

im

F

v

f,

dom

G

×

FCD

im

G

v

g,

im

F

6

dom

G

.

But

(

RLD

)

in

(

g

f

) =

l

a

×

RLD

c

a

×

FCD

c

atoms(

g

f

)

= (proposition

907

=

l

a

×

RLD

c

a

F

(Src

f

)

, c

F

(Dst

g

)

,

b

F

(Dst

f

) : (

a

×

FCD

b

atoms

f

b

×

FCD

c

atoms

g

)

=

l

a

×

RLD

c

a

F

(Src

f

)

, c

F

(Dst

g

)

,

b

0

, b

1

F

(Dst

f

) : (

a

×

FCD

b

atoms

f

b

×

FCD

c

atoms

g

b

0

6

b

1

)

.

Now it becomes obvious that (

RLD

)

in

g

(

RLD

)

in

f

= (

RLD

)

in

(

g

f

).

9.5. Complete funcoids and reloids

For the proof below assume

θ

=

l

x

Src

f

(

Src

f

{

x

} ×

RLD

h

f

i

@

{

x

}

)

7→

l

x

Src

f

(

Src

f

{

x

} ×

FCD

h

f

i

@

{

x

}

)

(where

f

ranges the set of complete funcoids).

Lemma

1119

.

θ

is a bijection from complete reloids into complete funcoids.

Proof.

Theorems

928

and

1039

.

Lemma

1120

.

(

FCD

)

g

=

θg

for every complete reloid

g

.