 17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

257

Theorem

1336

.

Q

(

C

)

g

Q

(

C

)

f

=

Q

(

C

)

i

n

(

g

i

f

i

) for every

n

-indexed

families

f

and

g

of composable morphisms of a quasi-invertible category with star-

morphisms.

Proof.

D

Q

(

C

)

i

n

(

g

i

f

i

)

E

a

=

StarComp(

a

;

λi

n

:

g

i

f

i

)

=

StarComp(StarComp(

a

;

f

);

g

) and

*

(

C

)

Y

g

(

C

)

Y

f

+

a

=

*

(

C

)

Y

g

+*

(

C

)

Y

f

+

a

= StarComp(StarComp(

a

;

f

);

g

)

.

The rest follows from symmetry.

Corollary

1337

.

Q

(

C

)

f

k

1

. . .

Q

(

C

)

f

0

=

Q

(

C

)

i

n

(

f

k

1

. . .

f

0

) for

every

n

-indexed families

f

0

, . . . , f

n

1

of composable morphisms of a quasi-invertible

category with star-morphisms.

Proof.

By math induction.

17.11.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

1338

.

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

1339

.

The group of small binary relations considered as a category

together with the set of of all

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

: id

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

.