:: T_0TOPSP semantic presentation

K54() is Element of K10(K50())

K50() is set

K10(K50()) is set

K49() is set

K10(K49()) is set

K10(K54()) is set

I[01] is non empty strict TopSpace-like TopStruct

the carrier of I[01] is non empty set

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

1 is non empty set

T is non empty set

T0 is non empty set

K11(T,T0) is Relation-like set

K10(K11(T,T0)) is set

K10(T) is set

f is non empty Relation-like T -defined T0 -valued Function-like V38(T) quasi_total Element of K10(K11(T,T0))

F is Element of K10(T)

f .: F is Element of K10(T0)

K10(T0) is set

f " (f .: F) is Element of K10(T)

R is set

f . R is set

TR is set

f . TR is set

T is TopStruct

the carrier of T is set

T0 is TopStruct

the carrier of T0 is set

K11( the carrier of T, the carrier of T0) is Relation-like set

K10(K11( the carrier of T, the carrier of T0)) is set

T is non empty TopStruct

the carrier of T is non empty set

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

K10( the carrier of T) is set

T0 is Relation-like the carrier of T -defined the carrier of T -valued Element of K10(K11( the carrier of T, the carrier of T))

f is set

F is set

R is set

[f,F] is set

[F,R] is set

[f,R] is set

TR is Element of the carrier of T

h is Element of the carrier of T

h is Element of K10( the carrier of T)

h is Element of the carrier of T

f is set

[f,f] is set

F is Element of K10( the carrier of T)

dom T0 is Element of K10( the carrier of T)

field T0 is set

f is set

F is set

[f,F] is set

[F,f] is set

R is Element of K10( the carrier of T)

f is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

F is Element of the carrier of T

R is Element of the carrier of T

[F,R] is set

TR is Element of K10( the carrier of T)

T0 is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

f is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

F is Element of the carrier of T

R is Element of the carrier of T

[F,R] is set

TR is Element of K10( the carrier of T)

TR is Element of K10( the carrier of T)

T is non empty TopStruct

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

T is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

(T) is TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

(T) is non empty TopSpace-like TopStruct

the carrier of (T) is non empty set

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

T is non empty TopSpace-like TopStruct

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

K10( the carrier of (T)) is set

the topology of T is non empty Element of K10(K10( the carrier of T))

K10( the carrier of T) is set

K10(K10( the carrier of T)) is set

T0 is Element of K10( the carrier of (T))

union T0 is set

K10((T)) is set

the topology of (T) is non empty Element of K10(K10( the carrier of (T)))

K10(K10( the carrier of (T))) is set

the topology of (space (T)) is non empty Element of K10(K10( the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K10( the carrier of (space (T))) is set

K10(K10( the carrier of (space (T)))) is set

T is non empty TopSpace-like TopStruct

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

F is set

R is Element of the carrier of T

Class ((T),R) is Element of K10( the carrier of T)

K10( the carrier of T) is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

T0 is Element of the carrier of T

(T) . T0 is Element of the carrier of (T)

Class ((T),T0) is Element of K10( the carrier of T)

K10( the carrier of T) is set

R is Element of the carrier of T

Class ((T),R) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

f is Element of the carrier of T

(T) . f is Element of the carrier of (T)

T0 is Element of the carrier of T

(T) . T0 is Element of the carrier of (T)

[f,T0] is Element of the carrier of K192(T,T)

K192(T,T) is non empty strict TopSpace-like TopStruct

the carrier of K192(T,T) is non empty set

Class ((T),T0) is Element of K10( the carrier of T)

K10( the carrier of T) is set

Class ((T),f) is Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

T0 is Element of K10( the carrier of T)

F is Element of the carrier of T

(T) . F is Element of the carrier of (T)

R is Element of the carrier of T

(T) . R is Element of the carrier of (T)

Class ((T),F) is Element of K10( the carrier of T)

[R,F] is Element of the carrier of K192(T,T)

K192(T,T) is non empty strict TopSpace-like TopStruct

the carrier of K192(T,T) is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

K10( the carrier of T) is set

(T) is non empty V4() a_partition of the carrier of T

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

T0 is Element of K10( the carrier of T)

F is Element of K10( the carrier of T)

R is set

TR is set

Class ((T),TR) is Element of K10( the carrier of T)

h is set

[R,TR] is set

[TR,R] is set

[h,TR] is set

[h,R] is set

T is non empty TopSpace-like TopStruct

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

the carrier of (T) is non empty set

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

K10( the carrier of T) is set

proj (T) is non empty Relation-like the carrier of T -defined (T) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T,(T)))

K11( the carrier of T,(T)) is Relation-like set

K10(K11( the carrier of T,(T))) is set

F is Element of K10( the carrier of T)

(T) .: F is Element of K10( the carrier of (T))

K10( the carrier of (T)) is set

R is Element of K10( the carrier of T)

K10((T)) is set

(T) " ((T) .: F) is Element of K10( the carrier of T)

union ((T) .: F) is set

the topology of T is non empty Element of K10(K10( the carrier of T))

K10(K10( the carrier of T)) is set

T is non empty TopSpace-like TopStruct

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

K10( the carrier of (T)) is set

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

F is Element of the carrier of (T)

R is Element of the carrier of (T)

F is Element of the carrier of (T)

R is Element of the carrier of (T)

TR is Element of the carrier of (space (T))

h is Element of the carrier of T

(T) . h is Element of the carrier of (T)

h is Element of the carrier of (space (T))

h is Element of the carrier of T

(T) . h is Element of the carrier of (T)

K10( the carrier of T) is set

H is Element of K10( the carrier of T)

(T) .: H is Element of K10( the carrier of (T))

x is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of (T)))

x .: H is Element of K10( the carrier of (T))

x . h is Element of the carrier of (T)

C is set

x . C is set

x . h is Element of the carrier of (T)

C is set

x . C is set

[h,h] is Element of the carrier of K192(T,T)

K192(T,T) is non empty strict TopSpace-like TopStruct

the carrier of K192(T,T) is non empty set

T is TopStruct

the carrier of T is set

K10( the carrier of T) is set

T0 is Element of the carrier of T

f is Element of the carrier of T

T0 is Element of the carrier of T

f is Element of the carrier of T

F is Element of the carrier of T

R is Element of the carrier of T

the non empty TopSpace-like TopStruct is non empty TopSpace-like TopStruct

( the non empty TopSpace-like TopStruct ) is non empty TopSpace-like TopStruct

( the non empty TopSpace-like TopStruct ) is non empty V4() a_partition of the carrier of the non empty TopSpace-like TopStruct

the carrier of the non empty TopSpace-like TopStruct is non empty set

( the non empty TopSpace-like TopStruct ) is Relation-like the carrier of the non empty TopSpace-like TopStruct -defined the carrier of the non empty TopSpace-like TopStruct -valued V38( the carrier of the non empty TopSpace-like TopStruct ) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of the non empty TopSpace-like TopStruct , the carrier of the non empty TopSpace-like TopStruct ))

K11( the carrier of the non empty TopSpace-like TopStruct , the carrier of the non empty TopSpace-like TopStruct ) is Relation-like set

K10(K11( the carrier of the non empty TopSpace-like TopStruct , the carrier of the non empty TopSpace-like TopStruct )) is set

Class ( the non empty TopSpace-like TopStruct ) is non empty V4() a_partition of the carrier of the non empty TopSpace-like TopStruct

space ( the non empty TopSpace-like TopStruct ) is non empty strict TopSpace-like TopStruct

the carrier of ( the non empty TopSpace-like TopStruct ) is non empty set

K10( the carrier of ( the non empty TopSpace-like TopStruct )) is set

T0 is Element of the carrier of ( the non empty TopSpace-like TopStruct )

f is Element of the carrier of ( the non empty TopSpace-like TopStruct )

T is non empty TopSpace-like TopStruct

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

K10( the carrier of (T)) is set

T0 is Element of the carrier of (T)

f is Element of the carrier of (T)

T0 is non empty TopSpace-like TopStruct

(T0) is non empty TopSpace-like TopStruct

(T0) is non empty V4() a_partition of the carrier of T0

the carrier of T0 is non empty set

(T0) is Relation-like the carrier of T0 -defined the carrier of T0 -valued V38( the carrier of T0) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T0, the carrier of T0))

K11( the carrier of T0, the carrier of T0) is Relation-like set

K10(K11( the carrier of T0, the carrier of T0)) is set

Class (T0) is non empty V4() a_partition of the carrier of T0

space (T0) is non empty strict TopSpace-like TopStruct

the carrier of (T0) is non empty set

T is non empty TopSpace-like TopStruct

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

K11( the carrier of (T0), the carrier of (T)) is Relation-like set

K10(K11( the carrier of (T0), the carrier of (T))) is set

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

(T0) is non empty Relation-like the carrier of T0 -defined the carrier of (T0) -valued Function-like V38( the carrier of T0) quasi_total continuous Element of K10(K11( the carrier of T0, the carrier of (T0)))

K11( the carrier of T0, the carrier of (T0)) is Relation-like set

K10(K11( the carrier of T0, the carrier of (T0))) is set

Proj (T0) is non empty Relation-like the carrier of T0 -defined the carrier of (space (T0)) -valued Function-like V38( the carrier of T0) quasi_total continuous Element of K10(K11( the carrier of T0, the carrier of (space (T0))))

the carrier of (space (T0)) is non empty set

K11( the carrier of T0, the carrier of (space (T0))) is Relation-like set

K10(K11( the carrier of T0, the carrier of (space (T0)))) is set

h is non empty Relation-like the carrier of (T0) -defined the carrier of (T) -valued Function-like V38( the carrier of (T0)) quasi_total Element of K10(K11( the carrier of (T0), the carrier of (T)))

h * (T0) is non empty Relation-like the carrier of T0 -defined the carrier of (T) -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of (T)))

K11( the carrier of T0, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T0, the carrier of (T))) is set

dom (T) is non empty Element of K10( the carrier of T)

K10( the carrier of T) is set

dom (h * (T0)) is non empty Element of K10( the carrier of T0)

K10( the carrier of T0) is set

h is Relation-like Function-like set

dom h is set

rng h is set

h * (h * (T0)) is Relation-like the carrier of (T) -valued Function-like set

K11( the carrier of T, the carrier of T0) is Relation-like set

K10(K11( the carrier of T, the carrier of T0)) is set

h is non empty Relation-like the carrier of T -defined the carrier of T0 -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of T0))

dom h is non empty Element of K10( the carrier of T)

[#] T is non empty non proper closed Element of K10( the carrier of T)

rng h is non empty Element of K10( the carrier of T0)

[#] T0 is non empty non proper closed Element of K10( the carrier of T0)

h " is non empty Relation-like the carrier of T0 -defined the carrier of T -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of T))

K11( the carrier of T0, the carrier of T) is Relation-like set

K10(K11( the carrier of T0, the carrier of T)) is set

rng h is non empty Element of K10( the carrier of (T))

K10( the carrier of (T)) is set

[#] (T) is non empty non proper closed Element of K10( the carrier of (T))

[#] (T0) is non empty non proper closed Element of K10( the carrier of (T0))

K10( the carrier of (T0)) is set

x is Element of K10( the carrier of T0)

h " x is Element of K10( the carrier of T)

(h * (T0)) .: x is Element of K10( the carrier of (T))

h " is non empty Relation-like the carrier of (T) -defined the carrier of (T0) -valued Function-like V38( the carrier of (T)) quasi_total Element of K10(K11( the carrier of (T), the carrier of (T0)))

K11( the carrier of (T), the carrier of (T0)) is Relation-like set

K10(K11( the carrier of (T), the carrier of (T0))) is set

p is Element of the carrier of T0

(h * (T0)) . p is Element of the carrier of (T)

x2 is Element of the carrier of T0

(h * (T0)) . x2 is Element of the carrier of (T)

(T0) . p is Element of the carrier of (T0)

h . ((T0) . p) is Element of the carrier of (T)

(T0) . x2 is Element of the carrier of (T0)

h . ((T0) . x2) is Element of the carrier of (T)

(T0) .: x is Element of K10( the carrier of (T0))

(h ") " ((T0) .: x) is Element of K10( the carrier of (T))

h .: ((T0) .: x) is Element of K10( the carrier of (T))

h " is Relation-like Function-like set

(h ") " ((T0) .: x) is set

(T) " ((h * (T0)) .: x) is Element of K10( the carrier of T)

(h * (T0)) " ((h * (T0)) .: x) is Element of K10( the carrier of T0)

h " ((h * (T0)) " ((h * (T0)) .: x)) is Element of K10( the carrier of T)

dom h is non empty Element of K10( the carrier of (T0))

h " is non empty Relation-like the carrier of (T) -defined the carrier of (T0) -valued Function-like V38( the carrier of (T)) quasi_total Element of K10(K11( the carrier of (T), the carrier of (T0)))

K11( the carrier of (T), the carrier of (T0)) is Relation-like set

K10(K11( the carrier of (T), the carrier of (T0))) is set

(h ") * (T) is non empty Relation-like the carrier of T -defined the carrier of (T0) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of (T0)))

K11( the carrier of T, the carrier of (T0)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T0))) is set

x is Element of K10( the carrier of T)

(h ") " x is Element of K10( the carrier of T0)

((h ") * (T)) .: x is Element of K10( the carrier of (T0))

p is Element of the carrier of T

((h ") * (T)) . p is Element of the carrier of (T0)

x2 is Element of the carrier of T

((h ") * (T)) . x2 is Element of the carrier of (T0)

(T) . p is Element of the carrier of (T)

(h ") . ((T) . p) is Element of the carrier of (T0)

(T) . x2 is Element of the carrier of (T)

(h ") . ((T) . x2) is Element of the carrier of (T0)

(T0) * h is non empty Relation-like the carrier of T -defined the carrier of (T0) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of (T0)))

h * ((T0) * h) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of (T)))

(h ") * h is non empty Relation-like the carrier of (T0) -defined the carrier of (T0) -valued Function-like V38( the carrier of (T0)) quasi_total Element of K10(K11( the carrier of (T0), the carrier of (T0)))

K11( the carrier of (T0), the carrier of (T0)) is Relation-like set

K10(K11( the carrier of (T0), the carrier of (T0))) is set

((h ") * h) * ((T0) * h) is non empty Relation-like the carrier of T -defined the carrier of (T0) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of (T0)))

id the carrier of (T0) is non empty Relation-like the carrier of (T0) -defined the carrier of (T0) -valued Function-like one-to-one V38( the carrier of (T0)) quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of K10(K11( the carrier of (T0), the carrier of (T0)))

(id the carrier of (T0)) * ((T0) * h) is non empty Relation-like the carrier of T -defined the carrier of (T0) -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of (T0)))

((h ") * (T)) * (h ") is non empty Relation-like the carrier of T0 -defined the carrier of (T0) -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of (T0)))

((T0) * h) * (h ") is non empty Relation-like the carrier of T0 -defined the carrier of (T0) -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of (T0)))

h * (h ") is non empty Relation-like the carrier of T0 -defined the carrier of T0 -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of T0))

(T0) * (h * (h ")) is non empty Relation-like the carrier of T0 -defined the carrier of (T0) -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of (T0)))

id the carrier of T0 is non empty Relation-like the carrier of T0 -defined the carrier of T0 -valued Function-like one-to-one V38( the carrier of T0) quasi_total onto bijective reflexive symmetric antisymmetric transitive Element of K10(K11( the carrier of T0, the carrier of T0))

(T0) * (id the carrier of T0) is non empty Relation-like the carrier of T0 -defined the carrier of (T0) -valued Function-like V38( the carrier of T0) quasi_total Element of K10(K11( the carrier of T0, the carrier of (T0)))

(T0) " (((h ") * (T)) .: x) is Element of K10( the carrier of T0)

((h ") * (T)) " (((h ") * (T)) .: x) is Element of K10( the carrier of T)

(h ") " (((h ") * (T)) " (((h ") * (T)) .: x)) is Element of K10( the carrier of T0)

(T) .: x is Element of K10( the carrier of (T))

h " ((T) .: x) is Element of K10( the carrier of (T0))

(h ") .: ((T) .: x) is Element of K10( the carrier of (T0))

(T0) " (h " ((T) .: x)) is Element of K10( the carrier of T0)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

T0 is non empty TopSpace-like T_0 TopStruct

the carrier of T0 is non empty set

K11( the carrier of T, the carrier of T0) is Relation-like set

K10(K11( the carrier of T, the carrier of T0)) is set

f is non empty Relation-like the carrier of T -defined the carrier of T0 -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of T0))

F is Element of the carrier of T

R is Element of the carrier of T

[F,R] is Element of the carrier of K192(T,T)

K192(T,T) is non empty strict TopSpace-like TopStruct

the carrier of K192(T,T) is non empty set

f . F is Element of the carrier of T0

f . R is Element of the carrier of T0

K10( the carrier of T0) is set

h is Element of K10( the carrier of T0)

f " h is Element of K10( the carrier of T)

K10( the carrier of T) is set

[#] T0 is non empty non proper closed Element of K10( the carrier of T0)

H is non empty Relation-like the carrier of T -defined the carrier of T0 -valued Function-like V38( the carrier of T) quasi_total Element of K10(K11( the carrier of T, the carrier of T0))

dom H is non empty Element of K10( the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

T0 is non empty TopSpace-like T_0 TopStruct

the carrier of T0 is non empty set

K11( the carrier of T, the carrier of T0) is Relation-like set

K10(K11( the carrier of T, the carrier of T0)) is set

f is non empty Relation-like the carrier of T -defined the carrier of T0 -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of T0))

F is Element of the carrier of T

Class ((T),F) is Element of K10( the carrier of T)

K10( the carrier of T) is set

f .: (Class ((T),F)) is Element of K10( the carrier of T0)

K10( the carrier of T0) is set

f . F is Element of the carrier of T0

{(f . F)} is non empty set

TR is set

h is set

f . h is set

[h,F] is set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

(T) is non empty TopSpace-like TopStruct

(T) is non empty V4() a_partition of the carrier of T

(T) is Relation-like the carrier of T -defined the carrier of T -valued V38( the carrier of T) quasi_total reflexive symmetric transitive Element of K10(K11( the carrier of T, the carrier of T))

K11( the carrier of T, the carrier of T) is Relation-like set

K10(K11( the carrier of T, the carrier of T)) is set

Class (T) is non empty V4() a_partition of the carrier of T

space (T) is non empty strict TopSpace-like TopStruct

the carrier of (T) is non empty set

(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (T)))

K11( the carrier of T, the carrier of (T)) is Relation-like set

K10(K11( the carrier of T, the carrier of (T))) is set

Proj (T) is non empty Relation-like the carrier of T -defined the carrier of (space (T)) -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of (space (T))))

the carrier of (space (T)) is non empty set

K11( the carrier of T, the carrier of (space (T))) is Relation-like set

K10(K11( the carrier of T, the carrier of (space (T)))) is set

T0 is non empty TopSpace-like T_0 TopStruct

the carrier of T0 is non empty set

K11( the carrier of T, the carrier of T0) is Relation-like set

K10(K11( the carrier of T, the carrier of T0)) is set

K11( the carrier of (T), the carrier of T0) is Relation-like set

K10(K11( the carrier of (T), the carrier of T0)) is set

f is non empty Relation-like the carrier of T -defined the carrier of T0 -valued Function-like V38( the carrier of T) quasi_total continuous Element of K10(K11( the carrier of T, the carrier of T0))

h is set

f .: h is Element of K10( the carrier of T0)

K10( the carrier of T0) is set

h is Element of the carrier of T

Class ((T),h) is Element of K10( the carrier of T)

K10( the carrier of T) is set

f . h is Element of the carrier of T0

{(f . h)} is non empty set

h is non empty Relation-like the carrier of (T) -defined the carrier of T0 -valued Function-like V38( the carrier of (T)) quasi_total Element of K10(K11( the carrier of (T), the carrier of T0))

h is non empty Relation-like the carrier of (T) -defined the carrier of T0 -valued Function-like V38( the carrier of (T)) quasi_total Element of K10(K11( the carrier of (T), the carrier of T0))

h is Element of the carrier of T

Class ((T),h) is Element of K10( the carrier of T)

K10( the carrier of T) is set

h . (Class ((T),h)) is set

f . h is Element of the carrier of T0

f .: (Class ((T),h)) is Element of K10( the carrier of T0)

K10( the carrier of T0) is set

{(f . h)} is non empty set

[#] T0 is non empty non proper closed Element of K10( the carrier of T0)

K10( the carrier of T0) is set

h is non empty Relation-like the carrier of (T) -defined the carrier of T0 -valued Function-like V38( the carrier of (T)) quasi_total Element of K10(K11( the carrier of (T), the carrier of T0))

h is Element of K10( the carrier of T0)

h " h is Element of K10( the carrier of (T))

K10( the carrier of (T)) is set

f " h is Element of K10( the carrier of T)

K10( the carrier of T) is set

union (h " h) is set

x is set

C is set

p is Element of the carrier of T

Class ((T),p) is Element of K10( the carrier of T)

dom f is non empty Element of K10( the carrier of T)

[x,p] is set

Class ((T),x) is Element of K10( the carrier of T)

h . C is set

f . x is set

h . (Class ((T),x)) is set

the topology of T is non empty Element of K10(K10( the carrier of T))

K10(K10( the carrier of T)) is set

h is non empty Relation-like the carrier of (T) -defined the carrier of T0 -valued Function-like V38( the carrier of (T)) quasi_total continuous Element of K10(K11( the carrier of (T), the carrier of T0))

h * (T) is non empty Relation-like the carrier of T -defined the carrier of T -defined the carrier of T0 -valued the carrier of T0 -valued Function-like V38( the carrier of T) V38( the carrier of T) quasi_total quasi_total continuous Element of K10(K11( the carrier of T, the carrier of T0))

x is set

f . x is set

(h * (T)) . x is set

Class ((T),x) is Element of K10( the carrier of T)

K10( the carrier of T) is set

dom (T) is non empty Element of K10( the carrier of T)

(T) . x is set

h . (Class ((T),x)) is set

f .: (Class ((T),x)) is Element of K10( the carrier of T0)

{(f . x)} is non empty set