 17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

259

Theorem

1345

.

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. Ob-

viously it is a funcoid

Q

i

n

Src

f

i

Q

i

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

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

dom

A

: Dst

f

i

defined by the formula

L

GR StarComp(

a

;

f

)

⇔ ∃

y

GR

a

Y

i

n

atoms

A

i

i

n

:

y

i

[

f

i

]

L

i

.

Theorem

1346

.

Let Dst

f

i

be a starrish join-semilattice for every

i

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

n

) is a free star, that is

X

(form

f

)

j

L

∪ {

(

j

;

X

)

} ∈

GR StarComp(

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

.