background image

21.10. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

341

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

)

(

λi

n

:

h

f

1

i

i

L

i

)

GR

a.

Theorem

1736

.

Let Src

f

i

be separable starrish join-semilattice and Dst

f

i

be

a starrish join-semilattice for every

i

n

for a set

n

. Let form

a

=

Q

i

n

(Src

f

i

).

1

. If

a

is a prestaroid then StarComp(

a, f

) is a prestaroid.

2

. If

a

is a staroid and Src

f

i

are strongly separable then StarComp(

a, f

) is

a staroid.

3

. If

a

is a completary staroid and then StarComp(

a, f

) is a completary

staroid.

Proof.

We have

f

1

i

(

X

t

Y

) =

f

1

i

X

t

f

1

i

Y

by theorem

1498

.

1

Let

L

Q

i

(arity

f

)

\{

k

}

(form

f

i

) for some

k

n

and

X, Y

form

f

k

. Then

X

t

Y

∈ h

StarComp(

a, f

)

i

k

L

λi

dom

f

:

f

1

i

X

t

Y

if

i

=

k

L

i

if

i

6

=

k

i

GR

a

λi

dom

f

:

f

1

i

X

t

f

1

i

Y

if

i

=

k

f

1

i

L

i

if

i

6

=

k

i

GR

a

f

1

i

X

t

f

1

i

Y

∈ h

a

i

k

(

λi

(dom

f

)

\ {

k

}

:

h

f

1

i

i

L

i

)

f

1

i

X

∈ h

a

i

k

(

λi

n

\ {

k

}

:

f

1

i

L

i

)

∨ h

f

1

i

i

Y

∈ h

a

i

k

(

λi

n

\ {

k

}

:

f

1

i

L

i

)

λi

dom

f

:

f

1

i

X

if

i

=

k

f

1

i

L

i

if

i

6

=

k

i

GR

a

λi

dom

f

:

f

1

i

Y

if

i

=

k

f

1

i

L

i

if

i

6

=

k

i

GR

a

λi

dom

f

:

f

1

i

X

if

i

=

k

L

i

if

i

6

=

k

i

GR

a

λi

dom

f

:

f

1

i

Y

if

i

=

k

L

i

if

i

6

=

k

i

GR

a

X

∈ h

StarComp(

a, f

)

i

k

L

Y

∈ h

StarComp(

a, f

)

i

k

L.

Thus StarComp(

a, f

) is a pre-staroid.

2

.

f

1

i

are monotone functions by the proposition

1497

Thus

f

1

i

X

i

v

f

1

i

Y

i

if

X, Y

Q

i

(arity

f

)

\{

k

}

(form

f

i

) and

X

v

Y

. So if

a

is a staroid and

X

GR StarComp(

a, f

) then (

λi

dom

f

:

h

f

1

i

i

X

i

)

GR

a

then (

λi

dom

f

:

h

f

1

i

i

Y

i

)

GR

a

that is

Y

GR StarComp(

a, f

).

3

.

L

0

t

L

1

GR StarComp(

a, f

)

(

λi

n

:

f

1

i

(

L

0

t

L

1

)

i

)

GR

a

(

λi

n

:

f

1

i

L

0

i

t h

f

1

i

i

L

1

i

)

GR

a

c

∈ {

0

,

1

}

: (

λi

n

:

f

1

i

L

c

(

i

)

i

)

GR

a

c

∈ {

0

,

1

}

: (

λi

n

:

L

c

(

i

)

i

)

GR StarComp(

a, f

)

.