17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

260

Let

X

0

t

X

1

Q

. Then there exist

y

Q

i

n

\{

j

}

atoms

A

i

,

y

0

(atoms

A

j

)

(val

a

)

j

(

y

|

n

\{

j

}

) such that

y

0

[

f

j

]

X

0

t

X

1

. Consequently (proposition

1072

)

y

0

[

f

j

]

X

0

y

0

[

f

j

]. But then

X

0

Q

X

1

Q

.

To finish the proof we need to show that GR StarComp(

a

;

f

) is an upper set,

but this is obvious.

2

Let

a

be a completary staroid. Let

L

0

t

L

1

GR StarComp(

a

;

f

) that

is

y

Q

i

n

atoms

A

i

: (

i

n

:

y

i

[

f

i

]

L

0

i

t

L

1

i

y

a

) that is

c

∈ {

0

,

1

}

n

, y

Q

i

n

atoms

A

i

:

i

n

:

y

i

[

f

i

]

L

c

(

i

)

i

y

a

(taken into account that Dst

f

i

is

starrish) that is

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR StarComp(

a

;

f

). So

StarComp(

a

;

f

) is a completary staroid.

Lemma

1347

.

b

6

Anch(

A

)

StarComp(

a

;

f

)

⇔ ∀

A

GR

a, B

GR

b, i

n

:

A

i

[

f

i

]

B

i

for anchored relations

a

and

b

, provided that Src

f

i

are atomic posets.

Proof.

b

6

Anch(

A

)

StarComp(

a

;

f

)

x

Anch(

A

)

\ {

0

}

: (

x

v

b

x

v

StarComp(

a

;

f

))

x

Anch(

A

)

\ {

0

}

: (

x

v

b

∧ ∀

B

GR

x

:

B

GR StarComp(

a

;

f

))

x

Anch(

A

)

\ {

0

}

:

x

v

b

∧ ∀

B

GR

x

A

Y

i

dom

A

atoms

A

i

: (

i

n

:

A

i

[

f

i

]

B

i

A

GR

a

)

!

x

Anch(

A

)

\ {

0

}

: (

x

v

b

∧ ∀

B

GR

x, A

GR

a, i

n

:

A

i

[

f

i

]

B

i

)

x

Anch(

A

) : (

x

v

b

∧ ∀

B

GR

x, A

GR

a, i

n

:

A

i

[

f

i

]

B

i

)

B

GR

b, A

GR

a, i

n

:

A

i

[

f

i

]

B

i

.

Theorem

1348

.

a

h

Q

(

C

)

f

i

b

⇔ ∀

A

a, B

b, i

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

1349

.

b

6

pStrd

(

A

)

StarComp(

a

;

f

)

b

6

pStrd

(

B

)

StarComp(

a

;

f

)

for staroids

a

and

b

.

FiXme

: What are

A

and

B

?

Theorem

1350

.

Anchored relations with objects being atomic posets and

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

6

StarComp(

a

;

f

)

a

6

StarComp(

b

;

f

)

(the rest is obvious).

Really,

1

.

L

GR StarComp(

a

;

f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

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

)

.