background image

21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

343

1

First prove that StarComp

(

a

)

(

a, f

) is a prestaroid. We need to prove that

(val StarComp

(

a

)

(

a, f

))

j

L

(for every

j

n

) is a free star, that is

(

X

(form

f

)

j

L

∪ {

(

j, X

)

} ∈

GR StarComp

(

a

)

(

a, f

)

)

is a free star, that is the following is a free star

X

(form

f

)

j

R

(

X

)

where

R

(

X

)

⇔ ∃

y

Q

i

n

atoms

A

i

: (

i

n

\ {

j

}

:

y

i

[

f

i

]

L

i

y

j

[

f

j

]

X

y

GR

a

).

R

(

X

)

y

Y

i

n

atoms

A

i

: (

i

n

\ {

j

}

:

y

i

[

f

i

]

L

i

y

j

[

f

j

]

X

y

j

(val

a

)

j

(

y

|

n

\{

j

}

))

y

Y

i

n

\{

j

}

atoms

A

i

, y

0

atoms

A

j

:

 

i

n

\ {

j

}

:

y

i

[

f

i

]

L

i

y

0

[

f

j

]

X

y

0

(val

a

)

j

(

y

|

n

\{

j

}

)

!

y

Y

i

n

\{

j

}

atoms

A

i

i

n

\ {

j

}

:

y

i

[

f

i

]

L

i

y

0

atoms

A

j

: (

y

0

[

f

j

]

X

y

0

(val

a

)

j

(

y

|

n

\{

j

}

))

.

If

y

Q

i

n

\{

j

}

atoms

A

i

i

n

\ {

j

}

:

y

i

[

f

i

]

L

i

is false our statement is

obvious. We can assume it is true.

So it is enough to prove that

(

X

(form

f

)

j

y

Q

i

n

\{

j

}

atoms

A

i

, y

0

atoms

A

j

: (

y

0

[

f

j

]

X

y

0

(val

a

)

j

(

y

|

n

\{

j

}

))

)

is a free star. That is

Q

=

(

X

(form

f

)

j

y

Q

i

n

\{

j

}

atoms

A

i

, y

0

(atoms

A

j

)

(val

a

)

j

(

y

|

n

\{

j

}

) :

y

0

[

f

j

]

X

)

is a free star.

(form

f

)

j

/

Q

is obvious. That

Q

is an upper set is obvious. It remains

to prove that

X

0

t

X

1

Q

X

0

Q

X

1

Q

for every

X

0

, X

1

(form

f

)

j

.

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

1499

)

y

0

[

f

j

]

X

0

y

0

[

f

j

]

X

1

. But then

X

0

Q

X

1

Q

.

To finish the proof we need to show that GR StarComp

(

a

)(

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

)

(

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

GR

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

GR

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

)

(

a, f

). So

StarComp

(

a

)

(

a, f

) is a completary staroid.

Lemma

1743

.

b

6

Anch(

B

)

StarComp

(

a

)

(

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.