 Proof.

If some

A

i

is empty, our statement is obvious. Let's assume

A

i

=

/

;

.

We need to prove that

i

2

dom

A

:

a

i

n

b

i

=

d

f

z

2

Q

A

j

a

v

b

t

z

g

.

To prove it is enough to show

a

i

n

b

i

=

d

f

z

i

j

z

2

Q

A

; a

v

b

t

z

g

that is

a

i

n

b

i

=

d

f

z

2

A

i

j

a

i

v

b

i

t

z

g

(for the reverse implication take

z

j

=

a

i

for

j

=

/

i

) what is true by denition.

Proposition 17.39.

If every

A

i

is a distributive lattice with least element, then

a

#

b

=

i

2

dom

A

:

a

i

#

b

i

for every

a; b

2

Q

A

whenever every

a

i

#

b

i

is dened.

Proof.

We need to prove that

i

2

dom

A

:

a

i

#

b

i

=

F

f

z

2

Q

A

j

z

v

a

^

z

b

g

.

To prove it is enough to show

a

i

#

b

i

=

F

f

z

i

j

z

2

Q

A

; z

v

a

^

z

b

g

that is

a

i

#

b

i

=

F

f

z

2

A

i

j

z

v

a

i

^ 8

j

2

dom

A

:

z

j

b

j

g

that is

a

i

#

b

i

=

F

f

z

2

A

i

j

z

v

a

i

^

z

b

i

g

(take

z

j

= 0

for

j

=

/

i

) what is true by denition.

Proposition 17.40.

Let every

A

i

be a poset with least element and

a

i

is dened. Then

a

=

i

2

dom

A

:

a

i

.

Proof.

We need to prove that

i

2

dom

A

:

a

i

=

F

f

c

2

A

j

c

a

g

. To prove this it is enough to

show that

a

i

=

F

f

c

i

j

c

2

Q

A

; c

a

g

that is

a

i

=

F

f

c

i

j

c

2

Q

A

;

8

j

2

dom

A

:

c

j

a

j

g

that is

a

i

=

F

f

c

i

j

c

2

Q

A

; c

i

a

i

g

(take

c

j

= 0

for

j

=

/

i

) that is

a

i

=

F

f

c

2

A

i

j

c

a

i

g

what is true by

denition.

Corollary 17.41.

Let every

A

i

be a poset with greatest element and

a

i

+

is dened. Then

a

+

=

i

2

dom

A

:

a

i

+

.

Proof.

By duality.

17.3 Denition of staroids

Let

n

be a set. As an example,

n

may be an ordinal,

n

may be a natural number, considered as a

set by the formula

n

=

f

0

; :::; n

¡

1

g

. Let

A

=

A

i

2

n

be a family of posets indexed by the set

n

.

Denition 17.42.

I will call an

anchored relation

a pair

f

= (

form

f

;

GR

f

)

of a family form

(

f

)

of

sets indexed by the some index set and a relation GR

(

f

)

2

P

Q

form

(

f

)

. I call GR

(

f

)

the

graph

of the anchored relation

f

. I denote Anch

(

A

)

the set of anchored relations of the form

A

.

Denition 17.43.

An anchored relation

on powersets

is an anchored relation

f

such that every

(

form

f

)

i

is a powerset.

I will denote arity

f

=

dom form

f

.

Denition 17.44.

Every set of anchored relations of the same form constitutes a poset by the

formula

f

v

g

,

GR

f

GR

g

.

Definition 17.45.

An anchored relation is an

anchored relation between posets

when every

(

form

f

)

i

is a poset.

Denition 17.46.

Let

f

be an anchored relation. For every

i

2

arity

f

and

L

2

Q

((

form

f

)

j

(

arity

f

)

nf

i

g

)

(

val

f

)

i

L

=

f

X

2

(

form

f

)

i

j

L

[ f

(

i

;

X

)

g 2

GR

f

g

(val is an abbreviation of the word value.)

Obvious 17.47.

X

2

(

val

f

)

i

L

,

L

[ f

(

i

;

X

)

g 2

GR

f

.

Proposition 17.48.

f

can be restored knowing form

(

f

)

and

(

val

f

)

i

for some

i

2

arity

f

.

Proof.

GR

f

=

f

K

2

Q

form

f

j

K

2

GR

f

g

=

f

L

[ f

(

i

;

X

)

g j

L

2

Q

(

form

f

)

j

(

arity

f

)

nf

i

g

;

X

2

(

form

f

)

i

; L

[ f

(

i

;

X

)

g 2

GR

f

g

=

f

L

[ f

(

i

;

X

)

g j

L

2

Q

(

form

f

)

j

(

arity

f

)

nf

i

g

; X

2

(

val

f

)

i

L

g

.

208

Multifuncoids and staroids