background image

7.7. DOMAIN AND RANGE OF A FUNCOID

157

Another proof of the above theorem (without atomic filters):

Proof.

h

f

(

g

t

h

)

iX

=

h

f

ih

g

t

h

iX

=

h

f

i

(

h

g

iX t h

h

iX

) =

h

f

ih

g

iX t h

f

ih

h

iX

=

h

f

g

iX t h

f

h

iX

=

h

f

g

t

f

h

iX

.

7.7. Domain and range of a funcoid

Definition

854

.

Let

A

be a set.

The

identity funcoid

1

FCD

A

=

(

A, A,

id

F

(

A

)

,

id

F

(

A

)

).

Obvious

855

.

The identity funcoid is a funcoid.

Proposition

856

.

[

f

] = [1

Dst

f

]

◦ h

f

i

for every funcoid

f

.

Proof.

From proposition

851

.

Definition

857

.

Let

A

be a set,

A ∈

F

(

A

). The

restricted identity funcoid

id

FCD

A

= (

A, A,

Au

,

Au

)

.

Proposition

858

.

The restricted identity funcoid is a funcoid.

Proof.

We need to prove that (

A u X

)

u Y 6

=

⊥ ⇔

(

A u Y

)

u X 6

=

what is

obvious.

Obvious

859

.

1

. (1

FCD

A

)

1

= 1

FCD

A

;

2

. (id

FCD

A

)

1

= id

FCD

A

.

Obvious

860

.

For every

X

,

Y ∈

F

(

A

)

1

.

X

1

FCD

A

Y ⇔ X u Y 6

=

;

2

.

X

h

id

FCD

A

i

Y ⇔ A u X u Y 6

=

.

Definition

861

.

I will define

restricting

of a funcoid

f

to a filter

A ∈

F

(Src

f

)

by the formula

f

|

A

=

f

id

FCD

A

.

Definition

862

.

Image

of a funcoid

f

will be defined by the formula im

f

=

h

f

i>

F

(Src

f

)

.

Domain

of a funcoid

f

is defined by the formula dom

f

= im

f

1

.

Obvious

863

.

For every morphism

f

Rel

(

A, B

) for sets

A

and

B

1

. im

FCD

f

=

im

f

;

2

. dom

FCD

f

=

dom

f

.

Proposition

864

.

h

f

iX

=

h

f

i

(

X u

dom

f

) for every funcoid

f

,

X ∈

F

(Src

f

).