17.8. INFINITE PRODUCT OF POSET ELEMENTS

248

Proof.

L

GR

Strd

(

A

)

Y

A

i

dom

A

:

A

i

6

L

i

i

(dom

A

)

\ {

k

}

:

A

i

6

L

i

L

k

6

A

k

L

k

*

FCD

(

A

)

Y

A

+

k

L

|

(dom

A

)

\{

k

}

L

GR

FCD

(

A

)

Y

A

.

Corollary

1300

.

Funcoidal product is a completary multifuncoid.

Proof.

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

Really,

L

i

6

*

FCD

(

A

)

Y

A

+

i

L

|

(dom

A

)

\{

i

}

⇔ ∀

i

dom

A

:

A

i

6

L

i

L

j

6

*

FCD

(

A

)

Y

A

+

j

L

|

(dom

A

)

\{

j

}

.

Theorem

1301

.

If our filtrator (

Q

A

;

Q

Z

) is with separable core and

A

Q

Z

,

then

Q

Strd

(

Z

)

A

=

Q

Strd

(

A

)

A

.

Proof.

GR

Strd

(

Z

)

Y

A

=

(

L

Q

A

up

L

Q

Strd

(

Z

)

A

)

=

L

Q

A

K

up

L, i

dom

A

:

A

i

6

K

i

=

L

Q

A

i

dom

A

, K

up

L

i

:

A

i

6

K

=

L

Q

A

i

dom

A

:

A

i

6

L

i

=

GR

Strd

(

A

)

Y

A.

Proposition

1302

.

Let (

Q

A

;

Q

Z

) be a meet-closed filtrator,

A

Q

Z

. Then

Q

Strd

(

A

)

A

=

Q

Strd

(

Z

)

A

.