Proposition 17.217.

X

h Q

(

A

)

f

i

Y , 8

i

2

dom

f

:

Pr

i

RLD

X

[

f

i

]

Pr

i

RLD

Y

for every indexed family

f

of funcoids and

X 2

RLD

(

Src

f

)

,

Y 2

RLD

(

Dst

f

)

.

Proof.

X

h Q

(

A

)

f

i

Y , 9

a

2

atoms

X

; b

2

atoms

Y

:

a

h Q

(

A

)

f

i

b

, 9

a

2

atoms

X

; b

2

atoms

Y8

i

2

dom

f

:

Pr

i

RLD

a

[

f

i

]

Pr

i

RLD

b

, 8

i

2

dom

f

9

x

2

atoms Pr

i

RLD

X

; y

2

atoms Pr

i

RLD

Y

:

x

i

[

f

i

]

y

i

, 8

i

2

dom

f

:

Pr

i

RLD

X

[

f

i

]

Pr

i

RLD

Y

.

Corollary 17.218.

X

f

(

A

)

g

Y ,

dom

X

[

f

]

dom

Y ^

im

X

[

g

]

im

Y

for funcoids

f

,

g

and reloids

X 2

RLD

(

Src

f

;

Src

g

)

, and

Y 2

RLD

(

Dst

f

;

Dst

g

)

.

Lemma 17.219.

For every

A

2

Rel

(

X

;

Y

)

(for every sets

X

,

Y

) we have:

f

(

dom

a

;

im

a

)

j

a

2

atoms

"

FCD

A

g

=

f

(

dom

a

;

im

a

)

j

a

2

atoms

"

RLD

A

g

:

Proof.

Let

x

2 f

(

dom

a

;

im

a

)

j

a

2

atoms

"

RLD

A

g

. Then

x

0

=

dom

a

and

x

1

=

im

a

where

a

2

atoms

"

RLD

A

.

Then

x

0

=

dom

(

FCD

)

a

and

x

1

=

im

(

FCD

)

a

and obviously

(

FCD

)

a

2

atoms

"

FCD

A

. So

x

2 f

(

dom

a

;

im

a

)

j

a

2

atoms

"

FCD

A

g

.

Let now

x

2 f

(

dom

a

;

im

a

)

j

a

2

atoms

"

FCD

A

g

. Then

x

0

=

dom

a

and

x

1

=

im

a

where

a

2

atoms

"

FCD

A

.

x

0

[

"

FCD

A

]

x

1

,

x

0

[(

FCD

)

"

RLD

A

]

x

1

,

x

0

RLD

x

1

/

"

RLD

A

. Thus there exists atomic reloid

x

0

such that

x

0

2

atoms

"

RLD

A

and dom

x

0

=

x

0

, im

x

0

=

x

1

.

So

x

2 f

(

dom

a

0

;

im

a

0

)

j

a

0

2

atoms

"

RLD

A

g

.

Theorem 17.220.

"

FCD

A

f

(

C

)

g

"

FCD

B

, "

RLD

A

f

(

A

)

g

"

RLD

B

for funcoids

f

,

g

, and Rel-

morphisms

A

:

Src

f

!

Src

g

, and

B

:

Dst

f

!

Dst

g

.

Proof.

"

FCD

A

f

(

C

)

g

"

FCD

B

, 9

a

2

atoms

"

FCD

A; b

2

atoms

"

FCD

B

:

a

f

(

C

)

g

b

,

9

a

2

atoms

"

FCD

A; b

2

atoms

"

FCD

B

: (

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

)

) 9

a

0

2

atoms dom

"

FCD

A;

a

1

2

atoms im

"

FCD

A; b

0

2

atoms dom

"

FCD

B ; b

1

2

atoms im

"

FCD

B

: (

a

0

[

f

]

b

0

^

a

1

[

g

]

b

1

)

.

On the other hand:

9

a

0

2

atoms dom

"

FCD

A; a

1

2

atoms im

"

FCD

A; b

0

2

atoms dom

"

FCD

B ; b

1

2

atoms im

"

FCD

B

:

(

a

0

[

f

]

b

0

^

a

1

[

g

]

b

1

)

) 9

a

0

2

atoms dom

"

FCD

A; a

1

2

atoms im

"

FCD

A; b

0

2

atoms dom

"

FCD

B ;

b

1

2

atoms im

"

FCD

B

: (

a

0

FCD

b

0

/

f

^

a

1

FCD

b

1

/

g

)

) 9

a

2

atoms

"

FCD

A; b

2

atoms

"

FCD

B

:

(

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

)

.

Also using the lemma we have

9

a

2

atoms

"

FCD

A; b

2

atoms

"

FCD

B

: (

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

)

, 9

a

2

atoms

"

RLD

A; b

2

atoms

"

RLD

B

: (

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

)

.

So

"

FCD

A

f

(

C

)

g

"

FCD

B

, 9

a

2

atoms

"

RLD

A; b

2

atoms

"

RLD

B

: (

dom

a

[

f

]

dom

b

^

im

a

[

g

]

im

b

)

, 9

a

2

atoms

"

RLD

A; b

2

atoms

"

RLD

B

:

a

f

(

A

)

g

b

, "

RLD

A

f

(

A

)

g

"

RLD

B

.

Corollary 17.221.

f

(

A

)

g

=

¡

f

(

C

)

g

where downgrading is taken on the ltrator

¡

FCD

(

FCD

(

Src

f

);

FCD

(

Dst

f

));

FCD

¡

P

Y

(

Src

f

);

P

Y

(

Dst

f

)

and upgrading is taken on the ltrator

¡

FCD

(

RLD

(

Src

f

);

RLD

(

Dst

f

));

FCD

¡

P

Y

(

Src

f

);

P

Y

(

Dst

f

)

:

where we equate

n

-ary relations with corresponding principal multifuncoids and principal mul-

tireloids, when appropriate.

Proof.

Leave as an exercise for the reader.

Conjecture 17.222.

"

FCD

A

h Q

(

C

)

f

i

"

FCD

B

, "

RLD

A

h Q

(

A

)

f

i

"

RLD

B

for every indexed family

f

of funcoids and

A

2

P

Q

i

2

dom

f

Src

f

i

,

B

2

P

Q

i

2

dom

f

Dst

f

i

.

17.15 Relationships between cross-composition and subatomic products

235