Proof.

L

2

GR

"

Strd

Q

A

,

up

L

GR

"

Strd

Q

A

, 8

X

2

up

L

:

Q

X

/

Q

A

, 8

X

2

up

L; i

2

dom

A

:

X

i

/

A

i

, 8

i

2

dom

A

:

L

i

/

"

F

A

i

,

L

2

GR

Q

i

2

dom

A

Strd

"

F

A

i

.

Corollary 17.98.

Staroidal product of principal lters is an upgraded principal staroid.

Proposition 17.99.

Q

Strd

a

=

Q

Strd

a

if each

a

i

2

A

i

(for

i

2

n

where

n

is some index set)

where

A

i

is a separable poset and

(

A

i

2

n

;

Z

i

2

n

)

is a down aligned ltrator.

Proof.

GR

Q

Strd

a

=

L

2

Q

A

j

up

L

Z

\

GR

Q

Strd

a

=

L

2

Q

A

j

up

L

GR

Q

Strd

a

=

L

2

Q

A

j 8

K

2

up

L

:

K

2

GR

Q

Strd

a

=

f

L

2

Q

A

j 8

K

2

up

L; i

2

n

:

K

i

/

a

i

g

=

f

L

2

Q

A

j 8

i

2

n;

K

2

up

L

:

K

i

/

a

i

g

=

f

L

2

Q

A

j 8

i

2

n

:

L

i

/

a

i

g

=

GR

Q

Strd

a

(taken into account that

Q

A

is a

separable poset).

Theorem 17.100.

Staroidal product is a completary staroid (if our posets are starrish join-

semilattices).

Proof.

We need to prove

8

i

2

dom

A

:

A

i

/ (

L

0

i

t

L

1

i

)

, 9

c

2 f

0

;

1

g

n

8

i

2

dom

A

:

A

i

/

L

c

(

i

)

i:

Really,

8

i

2

dom

A

:

A

i

/ (

L

0

i

t

L

1

i

)

, 8

i

2

dom

A

: (

A

i

/

L

0

i

_

A

i

/

L

1

i

)

, 9

c

2f

0

;

1

g

dom

A

8

i

2

dom

A

:

A

i

/

L

c

(

i

)

i

.

Denition 17.101.

Let

(

A

i

;

Z

i

)

be an indexed family of down-aligned ltrators.

Then for every

A

2

Q

A

funcoidal product

is multifuncoid

Q

FCD

(

A

)

A

dened by the formula

(for every

L

2

Q

Z

):

*

Y

FCD

(

A

)

A

+

k

L

=

A

k

if

8

i

2

(

dom

A

)

n f

k

g

:

A

i

/

L

i

0

otherwise

:

Proposition 17.102.

Q

Strd

(

A

)

A

=

h Q

FCD

(

A

)

A

i

.

Proof.

L

2

GR

Q

Strd

(

A

)

A

, 8

i

2

dom

A

:

A

i

/

L

i

, 8

i

2

(

dom

A

)

n f

k

g

:

A

i

/

L

i

^

L

k

/

A

k

,

L

k

/

DQ

FCD

(

A

)

A

E

k

L

j

(

dom

A

)

nf

k

g

,

L

2

GR

h Q

FCD

(

A

)

A

i

.

Corollary 17.103.

Funcoidal product is a completary multifuncoid.

Proof.

It is enough to prove that funcoidal product is a premultifuncoid. Really,

L

i

/

*

Y

FCD

(

A

)

A

+

i

L

j

(

dom

A

)

nf

i

g

,8

i

2

dom

A

:

A

i

/

L

i

,

L

j

/

*

Y

FCD

(

A

)

A

+

j

L

j

(

dom

A

)

nf

j

g

:

Theorem 17.104.

If our ltrator

(

Q

A

;

Q

Z

)

is with separable core and

A

2

Q

Z

, then

Q

Strd

(

Z

)

A

=

Q

Strd

(

A

)

A

.

Proof.

GR

Q

Strd

(

Z

)

A

=

n

L

2

Q

A

j

up

L

Q

Strd

(

Z

)

A

o

=

f

L

2

Q

A

j 8

K

2

up

L;

i

2

dom

A

:

A

i

/

K

i

g

=

f

L

2

Q

A

j 8

i

2

dom

A

; K

2

up

L

i

:

A

i

/

K

g

=

f

L

2

Q

A

j 8

i

2

dom

A

:

A

i

/

L

i

g

=

GR

Q

Strd

(

A

)

A

.

Proposition 17.105.

Let

(

Q

A

;

Q

Z

)

be a meet-closed ltrator,

A

2

Q

Z

. Then

Q

Strd

(

A

)

A

=

Q

Strd

(

Z

)

A

.

Proof.

GR

Q

Strd

(

A

)

A

=

GR

Q

Strd

(

A

)

A

=

f

L

2

Q

A

j 8

i

2

dom

A

:

A

i

/

L

i

g

=

f

L

2

Q

A

j 8

i

2

dom

A

:

A

i

/

L

i

g \

Q

Z

=

f

L

2

Q

Z

j 8

i

2

dom

A

:

A

i

/

L

i

g

=

GR

Q

Strd

(

Z

)

A

.

17.8 Infinite product of poset elements

215