background image

21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

340

Proof.

L

*

(

C

)

Y

f

+

Y

a

L

StarComp

Y

a, f

y

Y

a

i

n

:

y

i

f

i

L

i

y

Y

a

i

n

:

{

y

i

} 6

f

1

i

{

L

i

} ⇔

i

n

y

a

i

:

{

y

} 6

f

1

i

{

L

i

} ⇔

i

n

:

a

i

6

f

1

i

{

L

i

} ⇔

i

n

:

{

L

i

} 6 h

f

i

i

a

i

i

n

:

L

i

∈ h

f

i

i

a

i

L

Y

i

n

h

f

i

i

a

i

.

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

1732

.

b

6

StarComp(

a, f

)

⇔ ∃

x

a, y

b

j

n

:

x

j

GR(

f

j

)

y

j

.

Proof.

From the previous section.

Theorem

1733

.

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

: 1

Obj

m

i

) =

m

;

3

.

b

6

StarComp(

a, f

)

a

6

StarComp(

b, f

)

(the rest is obvious).

It follows from the previous section.

Proposition

1734

.

StarComp(

a

t

b, f

) = StarComp(

a, f

)

t

StarComp(

b, f

)

for an

n

-ary anchored relations

a

,

b

and an

n

-indexed family

f

of

Rel

-morphisms.

Proof.

It follows from the previous section.

Theorem

1735

.

Cross-composition product of a family of

Rel

-morphisms is a

principal funcoid.

Proof.

By the proposition and symmetry

Q

(

C

)

f

is a pointfree funcoid. Ob-

viously it is a funcoid

Q

i

n

Src

f

i

Q

i

n

Dst

f

i

. Its completeness (and dually

co-completeness) is obvious.