 Proposition 17.147.

StarComp

(

a

t

b

;

f

) =

StarComp

(

a

;

f

)

t

StarComp

(

b

;

f

)

for an

n

-ary

anchored relations

a

,

b

and an

n

-indexed family

f

of

Rel

-morphisms.

Proof.

It follows from the previous section.

Theorem 17.148.

Cross-composition product of a family of

Rel

-morphisms is a principal funcoid.

Proof.

By the proposition and symmetry

Q

(

C

)

f

is a pointfree funcoid. Obviously it is a funcoid

Q

i

2

n

Src

f

i

!

Q

i

2

n

Dst

f

i

. Its completeness (and dually co-completeness) is obvious.

17.11.5 Cross-composition product of funcoids

Let

a

be a an anchored relation of the form

A

and dom

A

=

n

.

Let every

f

i

(for all

i

2

n

) be a pointfree funcoid with Src

f

i

=

A

i

.

The star-composition of

a

with

f

is an anchored relation of the form

i

2

dom

A

:

Dst

f

i

dened

by the formula

L

2

GR StarComp

(

a

;

f

)

, 9

y

2

GR

a

\

Y

i

2

n

atoms

A

i

8

i

2

n

:

y

i

[

f

i

]

L

i

:

Theorem 17.149.

Let Dst

f

i

be a starrish join-semilattice for every

i

2

n

.

1. If

a

is a prestaroid then StarComp

(

a

;

f

)

is a staroid.

2. If

a

is a completary staroid and then StarComp

(

a

;

f

)

is a completary staroid.

Proof.

1. First prove that StarComp

(

a

;

f

)

is a prestaroid. We need to prove that

(

val StarComp

(

a

;

f

))

j

L

(for every

j

2

n

) is a free star, that is

f

X

2

(

form

f

)

j

j

L

[ f

(

j

;

X

)

g 2

GR StarComp

(

a

;

f

)

g

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

f

X

2

(

form

f

)

j

j

R

(

X

)

g

where

R

(

X

)

, 9

y

2

Q

i

2

n

atoms

A

i

: (

8

i

2

n

n f

j

g

:

y

i

[

f

i

]

L

i

^

y

j

[

f

j

]

X

^

y

2

GR

a

)

.

R

(

X

)

, 9

y

2

Q

i

2

n

atoms

A

i

: (

8

i

2

n

n f

j

g

:

y

i

[

f

i

]

L

i

^

y

j

[

f

j

]

X

^

y

j

2

(

val

a

)

j

(

y

j

n

nf

j

g

))

,

9

y

2

Q

i

2

n

nf

j

g

atoms

A

i

; y

0

2

atoms

A

j

: (

8

i

2

n

n f

j

g

:

y

i

[

f

i

]

L

i

^

y

0

[

f

j

]

X

^

y

0

2

(

val

a

)

j

(

y

j

n

nf

j

g

))

, 9

y

2

Q

i

2

n

nf

j

g

atoms

A

i

8

i

2

n

n f

j

g

:

y

i

[

f

i

]

L

i

^ 9

y

0

2

atoms

A

j

:

(

y

0

[

f

j

]

X

^

y

0

2

(

val

a

)

j

(

y

j

n

nf

j

g

))

.

If

9

y

2

Q

i

2

n

nf

j

g

atoms

A

i

8

i

2

n

n f

j

g

:

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

2

(

form

f

)

j

j 9

y

2

Y

i

2

n

nf

j

g

atoms

A

i

; y

0

2

atoms

A

j

: (

y

0

[

f

j

]

X

^

y

0

2

(

val

a

)

j

(

y

j

n

nf

j

g

))

)

is a free star. That is

Q

=

(

X

2

(

form

f

)

j

j 9

y

2

Y

i

2

n

nf

j

g

atoms

A

i

; y

0

2

(

atoms

A

j

)

\

(

val

a

)

j

(

y

j

n

nf

j

g

):

y

0

[

f

j

]

X

)

is a free star.

0

(

form

f

)

j

2

/

Q

is obvious. That

Q

is an upper set is obvious. It remains to prove

that

X

0

t

X

1

2

Q

)

X

0

2

Q

_

X

1

2

Q

for every

X

0

; X

1

2

(

form

f

)

j

. Let

X

0

t

X

1

2

Q

. Then

there exist

y

2

Q

i

2

n

nf

j

g

atoms

A

i

,

y

0

2

(

atoms

A

j

)

\

(

val

a

)

j

(

y

j

n

nf

j

g

)

such that

y

0

[

f

j

]

X

0

t

X

1

.

Consequently (proposition

15.16

)

y

0

[

f

j

]

X

0

_

y

0

[

f

j

]

X

1

. But then

X

0

2

Q

_

X

1

2

Q

.

To nish the proof we need to show that GR StarComp

(

a

;

f

)

is an upper set, but this

is obvious.

224

Multifuncoids and staroids