2. Let

a

be a completary staroid. Let

L

0

t

L

1

2

GR StarComp

(

a

;

f

)

that is

9

y

2

Q

i

2

n

atoms

A

i

:

(

8

i

2

n

:

y

i

[

f

i

]

L

0

i

t

L

1

i

^

y

2

a

)

that is

9

c

2 f

0

;

1

g

n

; y

2

Q

i

2

n

atoms

A

i

: (

8

i

2

n

:

y

i

[

f

i

]

L

c

(

i

)

i

^

y

2

a

)

(taken into account that Dst

f

i

is starrish) that is

9

c

2 f

0

;

1

g

n

:

(

i

2

n

:

L

c

(

i

)

i

)

2

GR StarComp

(

a

;

f

)

. So StarComp

(

a

;

f

)

is a completary staroid.

Lemma 17.150.

b

/

Anch

(

A

)

StarComp

(

a

;

f

)

, 8

A

2

GR

a; B

2

GR

b; i

2

n

:

A

i

[

f

i

]

B

i

for anchored

relations

a

and

b

, provided that Src

f

i

are atomic posets.

Proof.

b

/

Anch

(

A

)

StarComp

(

a

;

f

)

,

9

x

2

Anch

(

A

)

n f

0

g

: (

x

v

b

^

x

v

StarComp

(

a

;

f

))

,

9

x

2

Anch

(

A

)

n f

0

g

: (

x

v

b

^ 8

B

2

GR

x

:

B

2

GR StarComp

(

a

;

f

))

,

9

x

2

Anch

(

A

)

n f

0

g

:

x

v

b

^ 8

B

2

GR

x

9

A

2

Y

i

2

dom

A

atoms

A

i

: (

8

i

2

n

:

A

i

[

f

i

]

B

i

^

A

2

GR

a

)

!

,

9

x

2

Anch

(

A

)

n f

0

g

: (

x

v

b

^ 8

B

2

GR

x; A

2

GR

a; i

2

n

:

A

i

[

f

i

]

B

i

)

,

9

x

2

Anch

(

A

): (

x

v

b

^ 8

B

2

GR

x; A

2

GR

a; i

2

n

:

A

i

[

f

i

]

B

i

)

,

8

B

2

GR

b; A

2

GR

a; i

2

n

:

A

i

[

f

i

]

B

i

:

Theorem 17.151.

a

h Q

(

C

)

f

i

b

, 8

A

2

a; B

2

b; i

2

n

:

A

i

[

f

i

]

B

i

for anchored relations

a

and

b

,

provided that Src

f

i

and Dst

f

i

are atomic posets.

Proof.

From the lemma.

Conjecture 17.152.

b

/

pStrd

(

A

)

StarComp

(

a

;

f

)

,

b

/

pStrd

(

B

)

StarComp

(

a

;

f

)

for staroids

a

and

b

.

Theorem 17.153.

Anchored relations with objects being atomic posets and above dened com-

positions form a quasi-invertible category with star-morphisms.

Proof.

We need to prove:

1. StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

i

2

arity

m

:

g

i

f

i

);

2. StarComp

(

m

;

i

2

arity

m

:

id

Obj

m

i

) =

m

;

3.

b

/

StarComp

(

a

;

f

)

,

a

/

StarComp

(

b

;

f

y

)

(the rest is obvious).

Really,

1.

L

2

GR StarComp

(

a

;

f

)

, 9

y

2

GR

a

\

Q

i

2

n

atoms

A

i

8

i

2

n

:

y

i

[

f

i

]

L

i

.

Dene the relation

R

(

f

)

by the formula

xR

(

f

)

y

, 8

i

2

n

:

x

i

[

f

i

]

y

i

. Obviously

R

(

i

2

n

:

g

i

f

i

) =

R

(

g

)

R

(

f

)

:

L

2

GR StarComp

(

a

;

f

)

, 9

y

2

GR

a

\

Q

i

2

n

atoms

A

i

:

yR

(

f

)

L

.

L

2

GR StarComp

(

StarComp

(

a

;

f

);

g

)

, 9

p

2

GR StarComp

(

a

;

f

)

\

Q

i

2

n

atoms

A

i

:

pR

(

g

)

L

, 9

p; y

2

GR

a

\

Q

i

2

n

atoms

A

i

: (

yR

(

f

)

p

^

pR

(

g

)

L

)

, 9

y

2

GR

a

\

Q

i

2

n

atoms

A

i

:

y

(

R

(

g

)

R

(

f

))

L

, 9

y

2

GR

a

\

Q

i

2

n

atoms

A

i

:

y R

(

i

2

n

:

g

i

f

i

)

L

, 9

y

2

GR

a

\

Q

i

2

n

atoms

A

i

8

i

2

n

:

y

i

[

g

i

f

i

]

L

i

,

L

2

GR StarComp

(

a

;

i

2

n

:

g

i

f

i

)

because

p

2

GR StarComp

(

a

;

f

)

, 9

y

2

GR

a

\

Q

i

2

n

atoms

A

i

:

yR

(

f

)

p

.

2. Obvious.
3. It follows from the lemma above.

Theorem 17.154.

DQ

(

C

)

f

EQ

Strd

a

=

Q

i

2

n

Strd

h

f

i

i

a

i

for every families

f

=

f

i

2

n

of pointfree

funcoids between atomic posets and

a

=

a

i

2

n

where

a

i

2

Src

f

i

.

17.11 Product of an arbitrary number of funcoids

225