7.3. RELOIDAL PRODUCT OF FILTERS

136

G

g

F

F

atoms

f

=

g

f

x

RLD

(Src

f

; Dst

g

) :

x

6

g

f

x

6

G

g

F

F

atoms

f

x

RLD

(Src

f

; Dst

g

) : (

x

6

g

f

⇔ ∃

F

atoms

f

:

x

6

g

F

)

x

RLD

(Src

f

; Dst

g

) : (

g

1

x

6

f

⇔ ∃

F

atoms

f

:

g

1

x

6

F

)

what is obviously true.

Corollary

748

.

If

f

and

g

are composable reloids, then

g

f

=

G

G

F

F

atoms

f, G

atoms

g

.

Proof.

g

f

=

F

n

g

F

F

atoms

f

o

=

F

F

{

G

F

G

atoms

g

}

F

atoms

f

=

F

n

G

F

F

atoms

f,G

atoms

g

o

.

7.3. Reloidal product of filters

Definition

749

.

Reloidal product of filters

A

and

B

is defined by the formula

A ×

RLD

B

def

=

l

RLD

(Base(

A

);Base(

B

))

(

A

×

B

)

A

∈ A

, B

∈ B

.

Obvious

750

.

U

A

×

RLD

V

B

=

RLD

(

U

;

V

)

(

A

×

B

) for every sets

A

U

,

B

V

.

Theorem

751

.

A ×

RLD

B

=

F

n

a

×

RLD

b

a

atoms

A

,b

atoms

B

o

for every filters

A

and

B

.

Proof.

Obviously

A ×

RLD

B w

F

n

a

×

RLD

b

a

atoms

A

,b

atoms

B

o

.

Reversely, let

K

GR

F

n

a

×

RLD

b

a

atoms

A

,b

atoms

B

o

. Then

K

GR(

a

×

RLD

b

) for

every

a

atoms

A

,

b

atoms

B

.

K

X

a

×

Y

b

for some

X

a

a

,

Y

b

b

;

K

[

X

a

×

Y

b

a

atoms

A

, b

atoms

B

=

[

X

a

a

atoms

A

×

[

Y

b

b

atoms

B

A

×

B

where

A

∈ A

,

B

∈ B

;

K

GR(

A ×

RLD

B

).

Theorem

752

.

If

A

0

,

A

1

F

(

A

),

B

0

,

B

1

F

(

B

) for some sets

A

,

B

then

(

A

0

×

RLD

B

0

)

u

(

A

1

×

RLD

B

1

) = (

A

0

u A

1

)

×

RLD

(

B

0

u B

1

)

.

Proof.

(

A

0

×

RLD

B

0

)

u

(

A

1

×

RLD

B

1

) =

RLD

(

P

u

Q

)

P

xyGR(

A

0

×

RLD

B

0

)

, Q

xyGR(

A

1

×

RLD

B

1

)

=

RLD

(

A

;

B

)

((

A

0

×

B

0

)

(

A

1

×

B

1

))

A

0

∈ A

0

, B

0

∈ B

0

, A

1

∈ A

1

, B

1

∈ B

1

=

RLD

(

A

;

B

)

((

A

0

A

1

)

×

(

B

0

×

B

1

))

A

0

∈ A

0

, B

0

∈ B

0

, A

1

∈ A

1

, B

1

∈ B

1

=

RLD

(

A

;

B

)

(

K

×

L

)

K

∈ A

0

u A

1

, L

∈ B

0

u B

1

=

(

A

0

u A

1

)

×

RLD

(

B

0

u B

1

)

.