Then

8

X

2 h

Pr

i

i

GR

a; Y

2 h

Pr

i

i

GR

b

:

X

[

f

i

]

Y

.

Thus Pr

i

RLD

a

[

f

i

]

Pr

i

RLD

b

. So

8

i

2

dom

f

:

Pr

i

RLD

a

[

f

i

]

Pr

i

RLD

b

and thus

a

f

(

A

)

g

b

.

Remark 17.189.

It seems that the proof of the above theorem can be simplied using cross-

composition product.

Theorem 17.190.

Q

i

2

n

(

A

)

(

g

i

f

i

) =

Q

(

A

)

g

Q

(

A

)

f

for indexed (by an index set

n

) families

f

and

g

of funcoids such that

8

i

2

n

:

Dst

f

i

=

Src

g

i

.

Proof.

Let

a

,

b

be ultralters on

Q

i

2

n

Src

f

i

and

Q

i

2

n

Dst

g

i

correspondingly,

a

"

Y

i

2

n

(

A

)

(

g

i

f

i

)

#

b

, 8

i

2

dom

f

:

h

Pr

i

i

a

[

g

i

f

i

]

h

Pr

i

i

b

, 8

i

2

dom

f

9

C

2

atoms

F

(

Dst

f

i

)

: (

h

Pr

i

i

a

[

f

i

]

C

^

C

[

g

i

]

h

Pr

i

i

b

)

, 8

i

2

dom

f

9

c

2

atoms

RLD

(

i

2

n

:

Dst

f

)

: (

h

Pr

i

i

a

[

f

i

]

h

Pr

i

i

c

^ h

Pr

i

i

c

[

g

i

]

h

Pr

i

i

b

)

( 9

c

2

atoms

RLD

(

i

2

n

:

Dst

f

)

8

i

2

dom

f

: (

h

Pr

i

i

a

[

f

i

]

h

Pr

i

i

c

^ h

Pr

i

i

c

[

g

i

]

h

Pr

i

i

b

)

, 9

c

2

atoms

RLD

(

i

2

n

:

Dst

f

)

:

0

@

a

"

Y

(

A

)

f

#

c

^

c

"

Y

(

A

)

g

#

b

1

A

,

a

"

Y

(

A

)

g

Y

(

A

)

f

#

b:

Let

8

i

2

dom

f

9

c

2

atoms

RLD

(

i

2

n

:

Dst

f

)

: (

h

Pr

i

i

a

[

f

i

]

h

Pr

i

i

c

^ h

Pr

i

i

c

[

g

i

]

h

Pr

i

i

b

)

:

Then there exists

c

0

2

¡

atoms

RLD

(

i

2

n

:

Dst

f

)

n

such that

8

i

2

dom

f

: (

h

Pr

i

i

a

[

f

i

]

h

Pr

i

i

c

i

0

^ h

Pr

i

i

c

i

0

[

g

i

]

h

Pr

i

i

b

)

:

Then take

c

00

=

Q

RLD

c

0

. Then

8

i

2

dom

f

: (

h

Pr

i

i

a

[

f

i

]

h

Pr

i

i

c

i

00

^ h

Pr

i

i

c

i

00

[

g

i

]

h

Pr

i

i

b

)

. Thus

9

c

2

atoms

RLD

(

i

2

n

:

Dst

f

)

8

i

2

dom

f

: (

h

Pr

i

i

a

[

f

i

]

h

Pr

i

i

c

^ h

Pr

i

i

c

[

g

i

]

h

Pr

i

i

b

)

:

We have

a

h Q

i

2

n

(

A

)

(

g

i

f

i

)

i

b

,

a

h Q

(

A

)

g

Q

(

A

)

f

i

b

.

Corollary 17.191.

Q

(

A

)

f

k

¡

1

:::

Q

(

A

)

f

0

=

Q

i

2

n

(

A

)

(

f

k

¡

1

:::

f

0

)

for every

n

-indexed

families

f

0

; :::; f

n

¡

1

of composable funcoids.

Proposition 17.192.

Q

RLD

a

h Q

(

A

)

f

i Q

RLD

b

, 8

i

2

dom

f

:

a

i

[

f

i

]

b

i

for an indexed family

f

of

funcoids and indexed families

a

and

b

of lters where

a

i

2

F

(

Src

f

i

)

,

b

i

2

F

(

Dst

f

i

)

for every

i

2

dom

f

.

Proof.

If

a

i

= 0

or

b

i

= 0

for some

i

our theorem is obvious. We will take

a

i

=

/ 0

and

b

i

=

/ 0

, thus

there exist

x

2

atoms

Y

RLD

a;

y

2

atoms

Y

RLD

b:

Q

RLD

a

h Q

(

A

)

f

i Q

RLD

b

, 9

x

2

atoms

Q

RLD

a; y

2

atoms

Q

RLD

b

:

x

h Q

(

A

)

f

i

y

, 9

x

2

atoms

Q

RLD

a; y

2

atoms

Q

RLD

b

8

i

2

dom

f

:

h

Pr

i

i

x

[

f

i

]

h

Pr

i

i

y

, 8

i

2

dom

f

9

x

2

atoms

a

i

;

y

2

atoms

b

i

:

x

[

f

i

]

y

, 8

i

2

dom

f

:

a

i

[

f

i

]

b

i

.

Theorem 17.193.

DQ

(

A

)

f

E

x

=

Q

i

2

dom

f

RLD

h

f

i

i

Pr

i

RLD

x

for an indexed family

f

of funcoids and

x

2

atoms

RLD

(

i

2

dom

f

:

Src

f

i

)

for every

n

2

dom

f

.

Proof.

For every ultralter

y

2

F

¡ Q

i

2

dom

f

Dst

f

i

we have:

17.13 Subatomic product of funcoids

231