17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

262

Proposition

1354

.

Simple product is a pointfree funcoid

(

S

)

Y

f

FCD

Y

i

dom

f

Src

f

i

;

Y

i

dom

f

Dst

f

i

.

Proof.

Let

x

Q

i

dom

f

Src

f

i

and

y

Q

i

dom

f

Dst

f

i

. Then (take into

account that Src

f

i

and Dst

f

i

are posets with least elements)

y

6

λx

Y

i

dom

f

Src

f

i

:

λi

dom

f

:

h

f

i

i

x

i

x

y

6

λi

dom

f

:

h

f

i

i

x

i

i

dom

f

:

y

i

6 h

f

i

i

x

i

i

dom

f

:

x

i

6

f

1

i

y

i

x

6

λi

dom

f

:

f

1

i

y

i

x

6

λy

Y

i

dom

f

Dst

f

i

:

λi

dom

f

:

f

1

i

y

i

y.

Obvious

1355

.

D

Q

(

S

)

f

E

x

=

λi

dom

f

:

h

f

i

i

x

i

for

x

Q

Src

f

i

.

Obvious

1356

.

D

Q

(

S

)

f

E

x

i

=

h

f

i

i

x

i

for

x

Q

Src

f

i

.

Proposition

1357

.

f

i

can be restored if we know

Q

(

S

)

f

if

f

i

is a family of

pointfree funcoids between posets with least elements.

Proof.

Let’s restore the value of

h

f

i

i

x

where

i

dom

f

and

x

Src

f

i

.

Let

x

0

i

=

x

and

x

0

j

= 0 for

j

6

=

i

.

Then

h

f

i

i

x

=

h

f

i

i

x

0

i

=

D

Q

(

S

)

f

E

x

0

i

.

We have restored the value of

h

f

i

i

. Restoring the value of

f

1

i

is similar.

Remark

1358

.

In the above proposition it is not required that

f

i

are non-zero.

Proposition

1359

.

Q

(

S

)

g

Q

(

S

)

f

=

Q

(

S

)

i

n

(

g

i

f

i

) for

n

-indexed families

f

and

g

of composable pointfree funcoids between posets with least elements.

Proof.

*

(

S

)

Y

i

n

(

g

i

f

i

)

+

x

=

λi

dom

f

:

h

g

i

f

i

i

x

i

=

λi

dom

f

:

h

g

i

ih

f

i

i

x

i

=

*

(

S

)

Y

g

+

λi

dom

f

:

h

f

i

i

x

i

=

*

(

S

)

Y

g

+*

(

S

)

Y

f

+

x

=

*

(

S

)

Y

g

(

S

)

Y

f

+

x.

Thus

D

Q

(

S

)

i

n

(

g

i

f

i

)

E

=

D

Q

(

S

)

g

Q

(

S

)

f

E

.

Q

(

S

)

i

n

(

g

i

f

i

)

1

=

Q

(

S

)

g

Q

(

S

)

f

1

is similar.

Corollary

1360

.

Q

(

S

)

f

k

1

. . .

Q

(

S

)

f

0

=

Q

(

S

)

i

n

(

f

k

1

. . .

f

0

) for every

n

-indexed families

f

0

, . . . , f

n

1

of composable pointfree funcoids between posets

with least elements.