:: 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

the carrier of I[01] is non empty 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

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 ") " ((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