8.4. RESTRICTING RELOID TO A FILTER. DOMAIN AND IMAGE

189

Corollary

1023

.

(id

RLD

A

)

1

= id

RLD

A

.

Theorem

1024

.

f

|

A

=

f

id

RLD

A

for every reloid

f

and

A ∈

F

(Src

f

).

Proof.

We need to prove that

f

u

(

A ×

RLD

>

) =

f

RLD

(Src

f,

Src

f

)

l

id

A

A

up

A

.

We have

f

RLD

(Src

f,

Src

f

)

l

id

A

A

up

A

=

RLD

(Src

f,

Src

f

)

l

GR(

F

)

id

A

F

up

f, A

up

A

=

RLD

l

F

|

A

F

up

f, A

up

A

=

RLD

l

F

u

(

A

× >

T

(Dst

f

)

)

F

up

f, A

up

A

=

RLD

l

F

F

up

f

u

RLD

l

A

× >

T

(Dst

f

)

A

up

A

=

f

u

(

A ×

RLD

>

)

.

Theorem

1025

.

(

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

1026

.

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

).

Proof.

f

u

(

A ×

RLD

B

) =

f

u

(

A ×

RLD

>

F

(Dst

f

)

)

u

(

>

F

(Src

f

)

×

RLD

B

) =

f

|

A

u

(

>

F

(Src

f

)

×

RLD

B

) =

(

f

id

RLD

A

)

u

(

>

F

(Src

f

)

×

RLD

B

) =

((

f

id

RLD

A

)

1

u

(

>

F

(Src

f

)

×

RLD

B

)

1

)

1

=

((id

RLD

A

f

1

)

u

(

B ×

RLD

>

F

(Src

f

)

))

1

=

(id

RLD

A

f

1

id

RLD

B

)

1

=

id

RLD

B

f

id

RLD

A

.

Proposition

1027

.

id

B

id

A

= id

AuB

for all filters

A

,

B

(on some set

U

).

Proof.

id

B

id

A

= (id

B

)

|

A

= (1

RLD

U

|

B

)

|

A

= 1

RLD

U

|

AuB

= id

AuB

.

Theorem

1028

.

f

|

↑{

α

}

=

Src

f

{

α

} ×

RLD

im(

f

|

↑{

α

}

) for every reloid

f

and

α

Src

f

.