background image

6.6. DOMAIN AND RANGE OF A FUNCOID

108

For every

X ∈

F

(

A

),

Z ∈

F

(

C

)

X

[

f

(

g

t

h

)]

Z ⇔

y

atoms

F

(

B

)

: (

X

[

g

t

h

]

y

y

[

f

]

Z

)

y

atoms

F

(

B

)

: ((

X

[

g

]

y

∨ X

[

h

]

y

)

y

[

f

]

Z

)

y

atoms

F

(

B

)

: ((

X

[

g

]

y

y

[

f

]

Z

)

(

X

[

h

]

y

y

[

f

]

Z

))

y

atoms

F

(

B

)

: (

X

[

g

]

y

y

[

f

]

Z

)

∨ ∃

y

atoms

F

(

B

)

: (

X

[

h

]

y

y

[

f

]

Z

)

X

[

f

g

]

Z ∨ X

[

f

h

]

Z ⇔

X

[

f

g

t

f

h

]

Z

.

Remark

613

.

The above theorem can be proved without atomic filters by the

formula

FiXme

: This may be useful for a pointfree generalization. Preserve old proof

for history.

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

.

6.6. Domain and range of a funcoid

Definition

614

.

Let

A

be a set.

The

identity funcoid

id

FCD

(

A

)

=

(

A

;

A

; id

F

(

A

)

; id

F

(

A

)

).

Obvious

615

.

The identity funcoid is a funcoid.

Definition

616

.

Let

A

be a set,

A ∈

F

(

A

). The

restricted identity funcoid

id

FCD

A

= (

A

;

A

;

Au

;

Au

)

.

Proposition

617

.

The restricted identity funcoid is a funcoid.

Proof.

We need to prove that (

A u X

)

u Y 6

=

F

(

A

)

(

A u Y

)

u X 6

=

F

(

A

)

what is obvious.

Obvious

618

.

1

. (id

FCD

(

A

)

)

1

= id

FCD

(

A

)

;

2

. (id

FCD

A

)

1

= id

FCD

A

.

Obvious

619

.

For every

X

,

Y ∈

F

(

A

)

1

.

X

h

id

FCD

(

A

)

i

Y ⇔ X u Y 6

=

F

(

A

)

;

2

.

X

h

id

FCD

A

i

Y ⇔ A u X u Y 6

=

F

(

A

)

.

Definition

620

.

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

621

.

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

622

.

For every binary relation

f

between sets

A

and

B