21.8. ON PRODUCTS OF STAROIDS

334

2

From the lemma.

3

We need to prove

L

0

t

L

1

GR

(

D

)

Y

F

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

:

λi

arity

(

D

)

Y

F

:

L

c

(

i

)

i

GR

(

D

)

Y

F

for every

L

0

, L

1

Q

form

Q

(

D

)

F

that is

L

0

, L

1

Q

uncurry(form

F

).

Really

L

0

t

L

1

GR

Q

(

D

)

F

L

0

t

L

1

uncurry

z

z

Q

(GR

F

)

.

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

:

λi

arity

(

D

)

Y

F

:

L

c

(

i

)

i

GR

(

D

)

Y

F

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

:

λi

arity

(

D

)

Y

F

:

L

c

(

i

)

i

uncurry

z

z

Q

(GR

F

)

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

: curry

λi

arity

(

D

)

Y

F

:

L

c

(

i

)

i

Y

(GR

F

)

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

: curry

λ

(

i, j

)

arity

(

D

)

Y

F

:

L

c

(

i,j

)

(

i, j

)

Y

(GR

F

)

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

: (

λi

dom

F

: (

λj

dom

F

i

:

L

c

(

i,j

)

(

i, j

)))

Y

(GR

F

)

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

i

dom

F

: (

λj

dom

F

i

:

L

c

(

i,j

)

(

i, j

))

GR

F

i

i

dom

F

c

∈ {

0

,

1

}

dom

F

i

: (

λj

dom

F

i

:

L

c

(

j

)

(

i, j

))

GR

F

i

i

dom

F

c

∈ {

0

,

1

}

dom

F

i

: (

λj

dom

F

i

: (curry(

L

c

(

j

)

)

i

)

j

)

GR

F

i

i

dom

F

: curry(

L

0

)

i

t

curry(

L

1

)

i

GR

F

i

i

dom

F

: (curry(

L

0

)

t

curry(

L

1

))

i

GR

F

i

i

dom

F

: curry(

L

0

t

L

1

)

i

GR

F

i

L

0

t

L

1

uncurry

z

z

Q

(GR

F

)

L

0

t

L

1

GR

(

D

)

Y

F.

For staroids it is defined

ordinated product

Q

(ord)

as defined in the section

3.7.4

above.

Obvious

1705

.

If

f

and

g

are anchored relations and there exists a bijection

ϕ

from arity

g

to arity

f

such that

n

F

ϕ

F

GR

f

o

= GR

g

, then:

1

.

f

is a prestaroid iff

g

is a prestaroid.

2

.

f

is a staroid iff

g

is a staroid.

3

.

f

is a completary staroid iff

g

is a completary staroid.

Corollary

1706

.

Let

F

be an indexed family of anchored relations and every

(form

F

)

i

be a join-semilattice.