 Chapter 8
Relationships between funcoids and reloids

8.1 Funcoid induced by a reloid

Every reloid

f

induces a funcoid

(

FCD

)

f

2

FCD

(

Src

f

;

Dst

f

)

by the following formulas (for every

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

):

X

[(

FCD

)

f

]

Y , 8

F

2

xyGR

f

:

X

[

"

FCD

F

]

Y

;

h

(

FCD

)

f

iX

=

l

fh"

FCD

F

iX j

F

2

xyGR

f

g

:

We should prove that

(

FCD

)

f

is really a funcoid.

Proof.

We need to prove that

X

[(

FCD

)

f

]

Y , Y u h

(

FCD

)

f

iX

=

/ 0

F

(

Dst

f

)

, X u h

(

FCD

)

f

¡

1

iY

=

/ 0

F

(

Src

f

)

:

The above formula is equivalent to:

8

F

2

xyGR

f

:

X

[

"

FCD

F

]

Y ,

Y u

l

fh"

FCD

F

iX j

F

2

xyGR

f

g

=

/ 0

F

(

Dst

f

)

,

X u

l

fh"

FCD

F

¡

1

iY j

F

2

xyGR

f

g

=

/ 0

F

(

Src

f

)

:

We have

Y u

d

fh"

FCD

F

iX j

F

2

xyGR

f

g

=

d

fY u h"

FCD

F

iX j

F

2

xyGR

f

g

.

Let's denote

W

=

fY u h"

FCD

F

iX j

F

2

xyGR

f

g

.

8

F

2

xyGR

f

:

X

[

"

FCD

F

]

Y , 8

F

2

xyGR

f

:

Y u h"

FCD

F

iX

=

/ 0

F

(

Dst

f

)

,

0

F

(

Dst

f

)

2

/

W

.

We need to prove only that

0

F

(

Dst

f

)

2

/

W

,

d

W

=

/ 0

F

(

Dst

f

)

. (The rest follows from symmetry.)

This follows from the fact that

W

is a generalized lter base.

Let's prove that

W

is a generalized lter base. For this it's enough to prove that

V

=

fh"

FCD

F

iX j

F

2

xyGR

f

g

is a generalized lter base. Let

A

;

B 2

V

that is

A

=

h"

FCD

P

iX

,

B

=

h"

FCD

Q

iX

where

P ; Q

2

xyGR

f

. Then for

C

=

h"

FCD

(

P

u

Q

)

iX

is true both

C 2

V

and

C v A

;

B

. So

V

is a generalized lter base and thus

W

is a generalized lter base.

Proposition 8.1.

(

FCD

)

"

RLD

f

=

"

FCD

f

for every Rel-morphism

f

.

Proof.

X

[(

FCD

)

"

RLD

f

]

Y , 8

F

2

xyGR

"

RLD

f

:

X

[

"

FCD

F

]

Y , X

[

"

FCD

f

]

Y

(for every

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

).

Theorem 8.2.

X

[(

FCD

)

f

]

Y , X

RLD

/

f

for every reloid

f

and

X 2

F

(

Src

f

)

,

Y 2

F

(

Dst

f

)

.

Proof.

RLD

/

f

, 8

F

2

GR

f ; P

2 X

RLD

Y

:

P

/

F

, 8

F

2

GR

f ; X

2 X

; Y

2 Y

:

X

Y

/

F

, 8

F

2

GR

f ; X

2 X

; Y

2 Y

:

"

Src

f

X

"

FCD

(

Src

f

;

Dst

f

)

F

"

Dst

f

Y

, 8

F

2

GR

f

:

X

"

FCD

(

Src

f

;

Dst

f

)

F

Y

, X

[(

FCD

)

f

]

Y

:

131