7.17.

T

0

-,

T

1

-,

T

2

-,

T

3

-, AND

T

4

-SEPARABLE FUNCOIDS

180

Proof.

h

g

f

ih

µ

i

@

{

x

}

=

h

g

ih

f

ih

µ

i

@

{

x

} w

h

g

ih

ν

ih

f

i

@

{

x

} w

(using that

f

is monovalued and principal)

h

π

ih

g

ih

f

i

@

{

x

}

=

h

π

ih

g

f

i

@

{

x

}

.

Problem

966

.

Devise a pointfree (not using a particular point

x

) proof of the

above theorem. It should refer to a lemma which may use a particular point, but

the proof of the theorem itself should be without a particular point.

7.17.

T

0

-,

T

1

-,

T

2

-,

T

3

-, and

T

4

-separable funcoids

For funcoids it can be generalized

T

0

-,

T

1

-,

T

2

-, and

T

3

- separability. Worthwhile

note that

T

0

and

T

2

separability is defined through

T

1

separability.

Definition

967

.

Let call

T

1

-separable

such endofuncoid

f

that for every

α, β

Ob

f

is true

α

6

=

β

⇒ ¬

(@

{

α

}

[

f

]

@

{

β

}

)

.

Proposition

968

.

An endofuncoid

f

is

T

1

-separable iff Cor

f

v

1

FCD

Ob

f

.

Proof.

x, y

Ob

f

: (@

{

x

}

[

f

]

@

{

y

} ⇒

x

=

y

)

x, y

Ob

f

: (@

{

x

}

[Cor

f

]

@

{

y

} ⇒

x

=

y

)

Cor

f

v

1

FCD

Ob

f

.

Proposition

969

.

An endofuncoid

f

is

T

1

-separable iff Cor

h

f

i

{

x

} v {

x

}

for

every

x

Ob

f

.

Proof.

Cor

h

f

i

{

x

}

v

{

x

}

h

CoCompl

f

i

{

x

}

v

{

x

}

Compl CoCompl

f

v

1

FCD

Ob

f

Cor

f

v

1

FCD

Ob

f

.

Definition

970

.

Let call

T

0

-separable

such funcoid

f

FCD

(

A, A

) that

f

u

f

1

is

T

1

-separable.

Definition

971

.

Let call

T

2

-separable

such funcoid

f

that

f

1

f

is

T

1

-

separable.

For symmetric transitive funcoids

T

0

-,

T

1

- and

T

2

-separability are the same (see

theorem

252

).

Obvious

972

.

A funcoid

f

is

T

2

-separable iff

α

6

=

β

⇒ h

f

i

@

{

α

} 6 h

f

i

@

{

β

}

for every

α, β

Src

f

.

Definition

973

.

Funcoid

f

is

regular

iff for every

C

T

Dst

f

and

p

Src

f

h

f

ih

f

1

i

C

h

f

i

@

{

p

} ⇐↑

Src

f

{

p

}  h

f

1

i

C.

Proposition

974

.

The following are pairwise equivalent:

1

. A funcoid

f

is regular.

2

. Compl(

f

f

1

f

)

v

Compl

f

.

3

. Compl(

f

f

1

f

)

v

f

.