background image

17.13. SUBATOMIC PRODUCT OF FUNCOIDS

268

Proposition

1385

.

The funcoid

Q

(

A

)

f

exists.

Proof.

To prove that

Q

(

A

)

f

exists we need to prove (for every

a

atoms

RLD

(

λi

dom

f

:Src

f

i

)

,

b

atoms

RLD

(

λi

dom

f

:Dst

f

i

)

)

X

GR

a, Y

GR

b

x

atoms

RLD

(

λi

dom

f

:Src

f

i

)

, y

atoms

RLD

(

λi

dom

f

:Dst

f

i

)

Y

:

a

(

A

)

Y

f

b

a

(

A

)

Y

f

b.

Let

X

GR

a, Y

GR

b

x

atoms

RLD

(

λi

dom

f

:Src

f

i

)

X, y

atoms

RLD

(

λi

dom

f

:Dst

f

i

)

Y

:

a

(

A

)

Y

f

b.

Then

X

GR

a, Y

GR

b

x

atoms

RLD

(

λi

dom

f

:Src

f

i

)

X, y

atoms

RLD

(

λi

dom

f

:Dst

f

i

)

Y

:

RLD

Pr

i

x

(

A

)

Y

f

RLD

Pr

i

y.

Then because Pr

RLD

i

x

atoms

Src

f

i

Pr

i

X

and likewise for

y

:

X

GR

a, Y

GR

b

i

dom

f

x

atoms

Src

f

i

Pr

i

X, y

atoms

Dst

f

i

Pr

i

Y

:

x

[

f

i

]

y.

Thus

X

GR

a, Y

GR

b

i

dom

f

:

Src

f

i

Pr

i

X

[

f

i

]

Dst

f

i

Pr

i

Y

;

X

GR

a, Y

GR

b

i

dom

f

: Pr

i

X

[

f

i

]

Pr

i

Y

.

Then

X

∈ h

Pr

i

i

GR

a, Y

∈ h

Pr

i

i

GR

b

:

X

[

f

i

]

Y

.

Thus Pr

RLD

i

a

[

f

i

] Pr

RLD

i

b

. So

i

dom

f

:

RLD

Pr

i

a

[

f

i

]

RLD

Pr

i

b

and thus

a

h

Q

(

A

)

f

i

b

.

Remark

1386

.

It seems that the proof of the above theorem can be simplified

using cross-composition product.

Theorem

1387

.

Q

(

A

)

i

n

(

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

i

n

: Dst

f

i

= Src

g

i

.