 21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

339

21.10.3. Star composition of binary relations.

First define

star compo-

sition

for an

n

-ary relation

a

and an

n

-indexed family

f

of binary relations as an

n

-ary relation complying with the formulas:

Obj

StarComp(

a,f

)

=

{∗}

n

;

L

StarComp(

a, f

)

⇔ ∃

y

a

i

n

:

y

i

f

i

L

i

where

is a unique object of the group of small binary relations considered as a

category.

Proposition

1731

.

b

6

StarComp(

a, f

)

⇔ ∃

x

a, y

b

j

n

:

x

j

f

j

y

j

.

Proof.

b

6

StarComp(

a, f

)

⇔ ∃

y

: (

y

b

y

StarComp(

a, f

))

y

: (

y

b

∧ ∃

x

a

j

n

:

x

j

f

j

y

j

)

⇔ ∃

x

a, y

b

j

n

:

x

j

f

j

y

j

.

Theorem

1732

.

The group of small binary relations considered as a category

together with the set of of all small

n

-ary relations (for every small

n

) and the above

defined star-composition form a quasi-invertible category with star-morphisms.

Proof.

We need to prove:

1

. StarComp(StarComp(

m, f

)

, g

) = StarComp(

m, λi

n

:

g

i

f

i

);

2

. StarComp(

m, λi

arity

m

: 1

Obj

m

i

) =

m

;

3

.

b

6

StarComp(

a, f

)

a

6

StarComp(

b, f

) (the rest is obvious).

Really,

1

.

L

StarComp(

a, f

)

⇔ ∃

y

a

i

n

:

y

i

f

i

L

i

.

Define the relation

R

(

f

) by the formula

x R

(

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

:

y R

(

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

:

y R

(

f

)

p

.

2

Obvious.

3

It follows from the proposition above.

Obvious

1733

.

StarComp(

a

b, f

) = StarComp(

a, f

)

StarComp(

b, f

) for

n

-ary relations

a

,

b

and an

n

-indexed family

f

of binary relations.

Theorem

1734

.

D

Q

(

C

)

f

E

Q

a

=

Q

i

n

h

f

i

i

a

i

for every family

f

=

f

i

n

of

binary relations and

a

=

a

i

n

where

a

i

is a small set (for each

i

n

).