21.14. CROSS-COMPOSITION AND SUBATOMIC PRODUCTS

359

Proof.

FCD

A

h

f

×

(

C

)

g

i

FCD

B

a

atoms

FCD

A, b

atoms

FCD

B

:

a

h

f

×

(

C

)

g

i

b

a

atoms

FCD

A, b

atoms

FCD

B

: (dom

a

[

f

] dom

b

im

a

[

g

] im

b

)

a

0

atoms dom

FCD

A, a

1

atoms im

FCD

A,

b

0

atoms dom

FCD

B, b

1

atoms im

FCD

B

: (

a

0

[

f

]

b

0

a

1

[

g

]

b

1

)

.

On the other hand:

a

0

atoms dom

FCD

A, a

1

atoms im

FCD

A,

b

0

atoms dom

FCD

B, b

1

atoms im

FCD

B

: (

a

0

[

f

]

b

0

a

1

[

g

]

b

1

)

a

0

atoms dom

FCD

A, a

1

atoms im

FCD

A,

b

0

atoms dom

FCD

B, b

1

atoms im

FCD

B

: (

a

0

×

FCD

b

0

6

f

a

1

×

FCD

b

1

6

g

)

a

atoms

FCD

A, b

atoms

FCD

B

: (dom

a

[

f

] dom

b

im

a

[

g

] im

b

)

.

Also using the lemma we have

a

atoms

FCD

A, b

atoms

FCD

B

: (dom

a

[

f

] dom

b

im

a

[

g

] im

b

)

a

atoms

RLD

A, b

atoms

RLD

B

: (dom

a

[

f

] dom

b

im

a

[

g

] im

b

)

.

So

FCD

A

h

f

×

(

C

)

g

i

FCD

B

a

atoms

RLD

A, b

atoms

RLD

B

: (dom

a

[

f

] dom

b

im

a

[

g

] im

b

)

a

atoms

RLD

A, b

atoms

RLD

B

:

a

h

f

×

(

A

)

g

i

b

RLD

A

h

f

×

(

A

)

g

i

RLD

B.

Corollary

1815

.

f

×

(

A

)

g

=

(

f

×

(

C

)

g

) where downgrading is taken on

the filtrator

pFCD

(

FCD

(Src

f

)

,

FCD

(Dst

f

))

,

FCD

P

Y

(Src

f

)

,

P

Y

(Dst

f

)

and upgrading is taken on the filtrator

pFCD

(

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 multireloids, when appropriate.

Proof.

Leave as an exercise for the reader.

Conjecture

1816

.

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

P

Q

i

dom

f

Src

f

i

,

B

P

Q

i

dom

f

Dst

f

i

.

Theorem

1817

.

For every filters

a

0

,

a

1

,

b

0

,

b

1

we have

a

0

×

FCD

b

0

h

f

×

(

C

)

g

i

a

1

×

FCD

b

1

a

0

×

RLD

b

0

h

f

×

(

A

)

g

i

a

1

×

RLD

b

1

.