17.15. RELATIONSHIPS BETWEEN CROSS-COMPOSITION AND SUBATOMIC PRODUCTS

274

Proof.

a

h

f

×

(

C

)

g

i

b

a

f

1

6

g

1

b

(dom

a

×

FCD

im

a

)

f

1

6

g

1

(dom

b

×

FCD

im

b

)

h

f

i

dom

a

×

FCD

im

a

6

dom

b

×

FCD

g

1

im

b

h

f

i

dom

a

6

dom

b

im

a

6

g

1

im

b

dom

a

[

f

] dom

b

im

a

[

g

] im

b.

Proposition

1414

.

X

h

Q

(

A

)

f

i

Y ⇔ ∀

i

dom

f

: Pr

RLD

i

X

[

f

i

] Pr

RLD

i

Y

for

every indexed family

f

of funcoids and

X ∈

RLD

(Src

f

),

Y ∈

RLD

(Dst

f

).

Proof.

X

(

A

)

Y

f

Y ⇔

a

atoms

X

, b

atoms

Y

:

a

(

A

)

Y

f

b

a

atoms

X

, b

atoms

Y∀

i

dom

f

:

RLD

Pr

i

a

[

f

i

]

RLD

Pr

i

b

i

dom

f

x

atoms

RLD

Pr

i

X

, y

atoms

RLD

Pr

i

Y

:

x

i

[

f

i

]

y

i

i

dom

f

:

RLD

Pr

i

X

[

f

i

]

RLD

Pr

i

Y

.

Corollary

1415

.

X

f

×

(

A

)

g

Y ⇔

dom

X

[

f

] dom

Y ∧

im

X

[

g

] im

Y

for

funcoids

f

,

g

and reloids

X ∈

RLD

(Src

f

; Src

g

), and

Y ∈

RLD

(Dst

f

; Dst

g

).

Lemma

1416

.

For every

A

Rel

(

X

;

Y

) (for every sets

X

,

Y

) we have:

(dom

a

; im

a

)

a

atoms

FCD

A

=

(dom

a

; im

a

)

a

atoms

RLD

A

.

Proof.

Let

x

n

(dom

a

;im

a

)

a

atoms

RLD

A

o

. Then

x

0

= dom

a

and

x

1

= im

a

where

a

atoms

RLD

A

.

Then

x

0

= dom(

FCD

)

a

and

x

1

= im(

FCD

)

a

and obviously (

FCD

)

a

atoms

FCD

A

. So

x

n

(dom

a

;im

a

)

a

atoms

FCD

A

o

.

Let now

x

n

(dom

a

;im

a

)

a

atoms

FCD

A

o

. Then

x

0

= dom

a

and

x

1

= im

a

where

a

atoms

FCD

A

.

x

0

FCD

A

x

1

x

0

(

FCD

)

RLD

A

x

1

x

0

×

RLD

x

1

6↑

RLD

A

. Thus there

exists atomic reloid

x

0

such that

x

0

atoms

RLD

A

and dom

x

0

=

x

0

, im

x

0

=

x

1

.

So

x

n

(dom

a

0

;im

a

0

)

a

0

atoms

RLD

A

o

.

Theorem

1417

.

FCD

A

f

×

(

C

)

g

FCD

B

⇔↑

RLD

A

f

×

(

A

)

g

RLD

B

for

funcoids

f

,

g

, and

Rld

-morphisms

A

: Src

f

Src

g

, and

B

: Dst

f

Dst

g

.