 Really,

1.

L

StarComp

(

a

;

f

)

⇔ ∃

y

a

i

n

:

y

i

f

i

L

i

.

Define the relation

R

(

f

)

by the formula

xR

(

f

)

y

⇔ ∀

i

n

:

x

i

f

i

y

i

. Obviously

R

(

λi

n

:

g

i

f

i

) =

R

(

g

)

R

(

f

)

.

L

StarComp

(

a

;

f

)

⇔ ∃

y

a

:

yR

(

f

)

L

.

L

StarComp

(

StarComp

(

a

;

f

);

g

)

⇔ ∃

p

StarComp

(

a

;

f

):

p R

(

g

)

L

⇔ ∃

p, y

a

:

(

y R

(

f

)

p

p R

(

g

)

L

)

⇔ ∃

y

a

:

y

(

R

(

g

)

R

(

f

))

L

⇔ ∃

y

a

: (

y R

(

λi

n

:

g

i

f

i

)

L

)

L

StarComp

(

a

;

λi

n

:

g

i

f

i

)

because

p

StarComp

(

a

;

f

)

⇔ ∃

y

a

:

yR

(

f

)

p

.

2. Obvious.

3. It follows from the proposition above.

Theorem 135.

D

Q

(

C

)

f

E

Q

a

=

Q

i

n

h

f

i

i

a

i

for every families

f

=

f

i

n

of binary relations and

a

=

a

i

n

where

a

i

is a small set *(for each

i

n

).

Proof.

L

D

Q

(

C

)

f

E

Q

a

L

StarComp

(

Q

a

;

f

)

⇔ ∃

y

Q

a

i

n

:

y

i

f

i

L

i

⇔ ∃

y

Q

a

i

n

:

{

y

}

h

f

i

1

i{

L

i

} ⇔ ∀

i

n

y

a

i

:

{

y

}

h

f

i

1

i{

L

i

} ⇔ ∀

i

n

:

a

i

h

f

i

1

i{

L

i

} ⇔ ∀

i

n

:

{

L

i

}

h

f

i

i

a

i

⇔ ∀

i

n

:

L

i

∈ h

f

i

i

a

i

L

Q

i

n

h

f

i

i

a

i

.

11.5 Star composition of Rel-morphisms

Define

star composition

for an

n

-ary anchored relation

a

and an

n

-indexed family

f

of

Rel

-

morphisms as an

n

-ary anchored relation complying with the formulas:

Obj

StarComp

(

a

;

f

)

=

λi

arity

a

:

Dst

f

i

;

arity StarComp

(

a

;

f

) =

arity

a

;

L

GR StarComp

(

a

;

f

)

L

StarComp

(

GR

a

;

GR

f

)

.

(Here I denote GR

(

A

;

B

;

f

) =

f

for every

Rel

-morphism

f

.)

Proposition 136.

b

StarComp

(

a

;

f

)

⇔ ∃

x

a, y

b

j

n

:

x

j

f

j

y

j

.

Proof.

From the previous section.

Theorem 137.

Relations with above defined compositions form a quasi-invertible category with

star-morphisms.

Proof.

We need to prove:

1. StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

λi

arity

m

:

g

i

f

i

);

2. StarComp

(

m

;

λi

arity

m

:

id

Obj

m

i

) =

m

;

3.

b

StarComp

(

a

;

f

)

a

StarComp

(

b

;

f

)

(the rest is obvious).

It follows from the previous section.

Theorem 138.

Cross-composition product of a family of

Rel

-morphisms is a discrete funcoid.

Proof.

By the proposition and symmetry

Q

(

C

)

f

is a pointfree funcoid. Obviously it is a funcoid

Q

i

n

Src

f

i

Q

i

n

Dst

f

i

. Its completeness (and dually co-completeness) is obvious.

11.6 Cross-composition product of funcoids

Let

a

is a an anchored relation of the form

A

and dom

A

=

n

.

Let every

f

i

(for all

i

n

) is a pointfree funcoid with Src

f

i

=

A

i

.

Product of an arbitrary number of funcoids

21