 7.4. RESTRICTING RELOID TO A FILTER. DOMAIN AND IMAGE

138

Proof.

Let

K

GR

d

n

RLD

(Base(

A

);Base(

A

))

id

A

A

∈A

o

, then there exists

A

∈ A

such

that

K

id

A

. Then

id

RLD

A

v

RLD

(Base(

A

);Base(

A

))

id

Base(

A

)

u

(

A ×

RLD

>

F

(Dst

f

)

)

v

RLD

(Base(

A

);Base(

A

))

id

Base(

A

)

u

(

Base(

A

)

A

×

RLD

>

F

(Dst

f

)

) =

RLD

(Base(

A

);Base(

A

))

id

Base(

A

)

u ↑

RLD

(Base(

A

);Base(

A

))

(

A

×

Base(

A

)) =

RLD

(Base(

A

);Base(

A

))

(id

Base(

A

)

(

A

×

Base(

A

))) =

RLD

(Base(

A

);Base(

A

))

id

A

v

RLD

(Base(

A

);Base(

A

))

K.

Thus

K

GR id

RLD

A

.

Reversely let

K

GR id

RLD

A

= GR(id

RLD

(Base(

A

))

u

(

A ×

RLD

>

F

(Dst

f

)

)), then

there exists

A

∈ A

such that

K

GR

RLD

(Base(

A

);Base(

A

))

(id

Base(

A

)

(

A

×

Base(

A

))) =

GR

RLD

(Base(

A

);Base(

A

))

id

A

w

GR

l

RLD

(Base(

A

);Base(

A

))

id

A

A

∈ A

.

Corollary

763

.

(id

RLD

A

)

1

= id

RLD

A

.

Theorem

764

.

f

|

A

=

f

id

RLD

A

for every reloid

f

and

A ∈

F

(Src

f

).

Proof.

We need to prove that

f

u

(

RLD

>

F

(Dst

f

)

) =

f

d

n

RLD

(Src

f

;Src

f

)

id

A

A

∈A

o

.

We have

f

l

RLD

(Src

f

;Src

f

)

id

A

A

∈ A

=

l

RLD

(Src

f

;Src

f

)

(

F

id

A

)

F

GR

f, A

∈ A

=

l

RLD

(Src

f

;Src

f

)

(

F

|

A

)

F

GR

f, A

∈ A

=

l

RLD

(Src

f

;Src

f

)

(

F

(

A

×

Dst

f

))

F

GR

f, A

∈ A

=

l

RLD

(Src

f

;Src

f

)

F

F

GR

f

u

l

RLD

(Src

f

;Src

f

)

(

A

×

Dst

f

)

A

∈ A

=

f

u

(

A ×

RLD

>

F

(Dst

f

)

)

.

Theorem

765

.

(

g

f

)

|

A

=

g

(

f

|

A

) for every composable reloids

f

and

g

and

A ∈

F

(Src

f

).

Proof.

(

g

f

)

|

A

= (

g

f

)

id

RLD

A

=

g

(

f

id

RLD

A

) =

g

(

f

|

A

).

Theorem

766

.

f

u

(

A ×

RLD

B

) = id

RLD

B

f

id

RLD

A

for every reloid

f

and

A ∈

F

(Src

f

),

B ∈

F

(Dst

f

).