21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

345

L

GR StarComp

(

a

)

(

a, f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

:

y R

(

f

)

L

.

L

GR StarComp

(

a

)

(StarComp(

a, f

)

, g

)

p

GR StarComp

(

a

)

(

a, f

)

Y

i

n

atoms

(Dst

f

)

i

:

p R

(

g

)

L

p

Y

i

n

atoms

(Dst

f

)

i

, y

GR

a

Y

i

n

atoms

(Src

f

)

i

: (

y R

(

f

)

p

p R

(

g

)

L

)

y

GR

a

Y

i

n

atoms

(Src

f

)

i

:

y

(

R

(

g

)

R

(

f

))

L

y

GR

a

Y

i

n

atoms

(Src

f

)

i

:

y R

(

λi

n

:

g

i

f

i

)

L

y

GR

a

Y

i

n

atoms

(Src

f

)

i

y

i

n

:

y

i

[

g

i

f

i

]

L

i

L

GR StarComp

(

a

)

(

a, λi

n

:

g

i

f

i

)

because

p

GR StarComp

(

a

)

(

a, f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

(Src

f

)

i

y

:

y R

(

f

)

p

.

2

It follows from the lemma above.

Theorem

1752

.

D

Q

(

a

)

f

E

Q

Strd

a

=

Q

Strd

i

n

h

f

i

i

a

i

for every family

f

=

f

i

n

of

pointfree funcoids between atomic posets and

a

=

a

i

n

where

a

i

Src

f

i

.

Proof.

L

GR

*

(

a

)

Y

f

+

Strd

Y

a

L

GR StarComp

(

a

)

Strd

Y

a, f

!

y

Y

i

dom

A

atoms

A

i

i

n

: (

y

i

[

f

i

]

L

i

y

i

6

a

i

)

i

n

y

atoms

A

i

: (

y

[

f

i

]

L

i

y

6

a

i

)

i

n

:

a

i

[

f

i

]

L

i

i

n

:

L

i

6 h

f

i

i

a

i

L

GR

Strd

Y

i

n

h

f

i

i

a

i

.

Conjecture

1753

.

StarComp

(

a

)

(

a

t

b, f

)

=

StarComp

(

a

)

(

a, f

)

t

StarComp

(

a

)

(

b, f

) for anchored relations

a

,

b

of a form

A

, where every

A

i

is a distributive lattice, and an indexed family

f

of pointfree funcoids with

Src

f

i

=

A

i

.

21.10.7. Simple product of pointfree funcoids.

Definition

1754

.

Let

f

be an indexed family of pointfree funcoids with every

Src

f

i

and Dst

f

i

(for all

i

dom

f

) being a poset with least element.

Simple product

of

f

is

(

S

)

Y

f

=

λx

Y

i

dom

f

Src

f

i

:

λi

dom

f

:

h

f

i

i

x

i

, λy

Y

i

dom

f

Dst

f

i

:

λi

dom

f

:

f

1

i

y

i

.