:: T_1TOPSP semantic presentation

K87() is set
K10(K87()) is non empty set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
{} is set
the empty Function-like functional set is empty Function-like functional set
1 is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty with_non-empty_elements a_partition of the carrier of T
space S is non empty strict TopSpace-like TopStruct
the carrier of (space S) is non empty set
K10( the carrier of (space S)) is non empty set
Proj S is non empty Relation-like the carrier of T -defined the carrier of (space S) -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of (space S)) continuous Element of K10(K11( the carrier of T, the carrier of (space S)))
K11( the carrier of T, the carrier of (space S)) is non empty set
K10(K11( the carrier of T, the carrier of (space S))) is non empty set
f is Element of K10( the carrier of (space S))
(Proj S) " f is Element of K10( the carrier of T)
K10( the carrier of T) is non empty set
union f is set
K10(S) is non empty set
g1 is Element of K10(S)
(Proj S) " g1 is Element of K10( the carrier of T)
proj S is non empty Relation-like the carrier of T -defined S -valued Function-like V14( the carrier of T) V18( the carrier of T,S) Element of K10(K11( the carrier of T,S))
K11( the carrier of T,S) is non empty set
K10(K11( the carrier of T,S)) is non empty set
(proj S) " g1 is Element of K10( the carrier of T)
union g1 is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
K10( the carrier of T) is non empty set
S is non empty with_non-empty_elements a_partition of the carrier of T
space S is non empty strict TopSpace-like TopStruct
the carrier of (space S) is non empty set
K10( the carrier of (space S)) is non empty set
f is Element of K10( the carrier of (space S))
union f is set
g1 is Element of K10( the carrier of T)
K10(S) is non empty set
[#] T is non empty non proper closed Element of K10( the carrier of T)
([#] T) \ (union f) is Element of K10( the carrier of T)
union S is Element of K10( the carrier of T)
g2 is Element of K10(S)
union g2 is set
(union S) \ (union g2) is Element of K10( the carrier of T)
S \ f is Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
union (S \ f) is Element of K10( the carrier of T)
[#] (space S) is non empty non proper closed Element of K10( the carrier of (space S))
([#] (space S)) \ f is Element of K10( the carrier of (space S))
union (([#] (space S)) \ f) is set
x is Element of K10(S)
the topology of (space S) is non empty Element of K10(K10( the carrier of (space S)))
K10(K10( the carrier of (space S))) is non empty set
([#] T) \ g1 is Element of K10( the carrier of T)
the topology of T is non empty Element of K10(K10( the carrier of T))
([#] T) \ g1 is Element of K10( the carrier of T)
the topology of T is non empty Element of K10(K10( the carrier of T))
x is Element of K10(S)
the topology of (space S) is non empty Element of K10(K10( the carrier of (space S)))
K10(K10( the carrier of (space S))) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
f is set
g1 is non empty with_non-empty_elements a_partition of the carrier of T
bool (bool the carrier of T) is non empty Element of K10(K10((bool the carrier of T)))
f is set
g1 is non empty with_non-empty_elements a_partition of the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ the carrier of T} is set
S is non empty with_non-empty_elements a_partition of the carrier of T
g1 is Element of K10( the carrier of T)
[#] T is non empty non proper closed 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 partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
(T) is TopSpace-like TopStruct
the carrier of T is non empty set
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
(T) is non empty strict TopSpace-like TopStruct
the carrier of T is non empty set
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
the carrier of (T) is non empty set
K10((Intersection (T))) is non empty set
S is Element of the carrier of (T)
{S} is Element of K10( the carrier of (T))
K10( the carrier of (T)) is non empty set
(Intersection (T)) \ {S} is Element of K10(K10( the carrier of T))
g1 is Element of the carrier of T
EqClass (g1,(Intersection (T))) is Element of K10( the carrier of T)
{ (EqClass (g1,b₁)) where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ in (T) } is set
x is set
y is non empty with_non-empty_elements a_partition of the carrier of T
EqClass (g1,y) is Element of K10( the carrier of T)
x is set
y is non empty with_non-empty_elements a_partition of the carrier of T
EqClass (g1,y) is Element of K10( the carrier of T)
x is non empty Element of K10(K10( the carrier of T))
y is non empty Element of K10(K10( the carrier of T))
y is Element of K10( the carrier of T)
ty is non empty with_non-empty_elements a_partition of the carrier of T
EqClass (g1,ty) is Element of K10( the carrier of T)
h is non empty with_non-empty_elements a_partition of the carrier of T
meet { (EqClass (g1,b₁)) where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ in (T) } is set
g2 is Element of K10( the carrier of T)
[#] T is non empty non proper closed Element of K10( the carrier of T)
([#] T) \ g2 is Element of K10( the carrier of T)
([#] T) \ S is Element of K10( the carrier of T)
the topology of T is non empty Element of K10(K10( the carrier of T))
union ((Intersection (T)) \ {S}) is Element of K10( the carrier of T)
f is Element of K10((Intersection (T)))
{ b₁ where b₁ is Element of K10((Intersection (T))) : union b₁ in the topology of T } is set
the carrier of (space (Intersection (T))) is non empty set
K10( the carrier of (space (Intersection (T)))) is non empty set
y is Element of K10( the carrier of (space (Intersection (T))))
the topology of (space (Intersection (T))) is non empty Element of K10(K10( the carrier of (space (Intersection (T)))))
K10(K10( the carrier of (space (Intersection (T))))) is non empty set
ty is Element of K10( the carrier of (T))
[#] (T) is non empty non proper closed Element of K10( the carrier of (T))
([#] (T)) \ {S} is Element of K10( the carrier of (T))
T is non empty TopSpace-like TopStruct
(T) is non empty strict TopSpace-like TopStruct
the carrier of T is non empty set
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
the non empty TopSpace-like TopStruct is non empty TopSpace-like TopStruct
( the non empty TopSpace-like TopStruct ) is non empty strict TopSpace-like T_0 T_1 TopStruct
the carrier of the non empty TopSpace-like TopStruct is non empty set
( the non empty TopSpace-like TopStruct ) is non empty partition-membered Element of K10(K10((bool the carrier of the non empty TopSpace-like TopStruct )))
bool the carrier of the non empty TopSpace-like TopStruct is non empty Element of K10(K10( the carrier of the non empty TopSpace-like TopStruct ))
K10( the carrier of the non empty TopSpace-like TopStruct ) is non empty set
K10(K10( the carrier of the non empty TopSpace-like TopStruct )) is non empty set
K10((bool the carrier of the non empty TopSpace-like TopStruct )) is non empty set
K10(K10((bool the carrier of the non empty TopSpace-like TopStruct ))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of the non empty TopSpace-like TopStruct : b₁ is closed } is set
Intersection ( the non empty TopSpace-like TopStruct ) is non empty with_non-empty_elements a_partition of the carrier of the non empty TopSpace-like TopStruct
space (Intersection ( the non empty TopSpace-like TopStruct )) is non empty strict TopSpace-like TopStruct
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
Proj (Intersection (T)) is non empty Relation-like the carrier of T -defined the carrier of (space (Intersection (T))) -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of (space (Intersection (T)))) continuous Element of K10(K11( the carrier of T, the carrier of (space (Intersection (T)))))
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
the carrier of (space (Intersection (T))) is non empty set
K11( the carrier of T, the carrier of (space (Intersection (T)))) is non empty set
K10(K11( the carrier of T, the carrier of (space (Intersection (T))))) is non empty set
(T) is non empty strict TopSpace-like T_0 T_1 TopStruct
the carrier of (T) is non empty set
K11( the carrier of T, the carrier of (T)) is non empty set
K10(K11( the carrier of T, the carrier of (T))) is non empty set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
K10( the carrier of T) is non empty set
f is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of S) continuous Element of K10(K11( the carrier of T, the carrier of S))
rng f is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
{ (f " {b₁}) where b₁ is Element of the carrier of S : b₁ in rng f } is set
dom f is Element of K10( the carrier of T)
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10(K10( the carrier of T)) is non empty set
g1 is set
g2 is Element of the carrier of S
{g2} is Element of K10( the carrier of S)
f " {g2} is Element of K10( the carrier of T)
g1 is Element of K10(K10( the carrier of T))
g2 is Element of K10(K10( the carrier of T))
x is Element of K10( the carrier of T)
y is Element of the carrier of S
{y} is Element of K10( the carrier of S)
f " {y} is Element of K10( the carrier of T)
y is set
f . y is set
{(f . y)} is set
ty is Element of K10( the carrier of T)
h is Element of the carrier of S
{h} is Element of K10( the carrier of S)
f " {h} is Element of K10( the carrier of T)
h is set
f . h is set
union g2 is Element of K10( the carrier of T)
x is set
f . x is set
y is set
y is Element of the carrier of S
{y} is Element of K10( the carrier of S)
f " {y} is Element of K10( the carrier of T)
{(f . x)} is set
g1 is Element of K10( the carrier of T)
g2 is Element of the carrier of S
{g2} is Element of K10( the carrier of S)
f " {g2} is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
f is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of S) continuous Element of K10(K11( the carrier of T, the carrier of S))
rng f is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
{ (f " {b₁}) where b₁ is Element of the carrier of S : b₁ in rng f } is set
g2 is set
x is Element of the carrier of T
EqClass (x,(Intersection (T))) is Element of K10( the carrier of T)
f . x is Element of the carrier of S
{(f . x)} is Element of K10( the carrier of S)
f " {(f . x)} is Element of K10( the carrier of T)
g1 is non empty with_non-empty_elements a_partition of the carrier of T
y is Element of K10( the carrier of T)
EqClass (x,g1) is Element of K10( the carrier of T)
{ (EqClass (x,b₁)) where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ in (T) } is set
dom f is Element of K10( the carrier of T)
y is Element of the carrier of S
{y} is Element of K10( the carrier of S)
f " {y} is Element of K10( the carrier of T)
y is set
meet { (EqClass (x,b₁)) where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ in (T) } is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
(T) is non empty strict TopSpace-like T_0 T_1 TopStruct
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
the carrier of (T) is non empty set
f is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of S) continuous Element of K10(K11( the carrier of T, the carrier of S))
rng f is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
g1 is set
g2 is Element of the carrier of T
EqClass (g2,(Intersection (T))) is Element of K10( the carrier of T)
x is Element of the carrier of T
f . x is Element of the carrier of S
y is Element of the carrier of S
{y} is Element of K10( the carrier of S)
f " {y} is Element of K10( the carrier of T)
dom f is Element of K10( the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
(T) is non empty strict TopSpace-like T_0 T_1 TopStruct
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
the carrier of (T) is non empty set
K11( the carrier of (T), the carrier of S) is non empty set
K10(K11( the carrier of (T), the carrier of S)) is non empty set
(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of (T)) continuous Element of K10(K11( the carrier of T, the carrier of (T)))
K11( the carrier of T, the carrier of (T)) is non empty set
K10(K11( the carrier of T, the carrier of (T))) is non empty set
Proj (Intersection (T)) is non empty Relation-like the carrier of T -defined the carrier of (space (Intersection (T))) -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of (space (Intersection (T)))) continuous Element of K10(K11( the carrier of T, the carrier of (space (Intersection (T)))))
the carrier of (space (Intersection (T))) is non empty set
K11( the carrier of T, the carrier of (space (Intersection (T)))) is non empty set
K10(K11( the carrier of T, the carrier of (space (Intersection (T))))) is non empty set
f is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of S) continuous Element of K10(K11( the carrier of T, the carrier of S))
dom (T) is Element of K10( the carrier of T)
rng f is Element of K10( the carrier of S)
K10( the carrier of S) is non empty set
{ (f " {b₁}) where b₁ is Element of the carrier of S : b₁ in rng f } is set
dom f is Element of K10( the carrier of T)
x is set
y is Element of the carrier of T
EqClass (y,(Intersection (T))) is Element of K10( the carrier of T)
y is Element of the carrier of T
f . y is Element of the carrier of S
{(f . y)} is Element of K10( the carrier of S)
f " {(f . y)} is Element of K10( the carrier of T)
h is Element of the carrier of S
{h} is Element of K10( the carrier of S)
f " {h} is Element of K10( the carrier of T)
h is Element of the carrier of S
{h} is Element of K10( the carrier of S)
f " {h} is Element of K10( the carrier of T)
g2 is non empty with_non-empty_elements a_partition of the carrier of T
c₁₂ is set
x is Relation-like Function-like set
dom x is set
g2 is non empty with_non-empty_elements a_partition of the carrier of T
y is set
y is Element of the carrier of S
{y} is Element of K10( the carrier of S)
f " {y} is Element of K10( the carrier of T)
ty is Element of the carrier of S
{ty} is Element of K10( the carrier of S)
f " {ty} is Element of K10( the carrier of T)
h is set
f . h is set
y is Relation-like Function-like set
dom y is set
x * y is Relation-like Function-like set
dom (x * y) is set
ty is set
h is Element of the carrier of S
{h} is Element of K10( the carrier of S)
f " {h} is Element of K10( the carrier of T)
x . ty is set
(T) * (x * y) is Relation-like Function-like set
dom ((T) * (x * y)) is set
ty is set
(T) . ty is set
rng (T) is Element of K10( the carrier of (T))
K10( the carrier of (T)) is non empty set
ty is set
f . ty is set
((T) * (x * y)) . ty is set
(T) . ty is set
rng (T) is Element of K10( the carrier of (T))
K10( the carrier of (T)) is non empty set
h is Element of the carrier of T
EqClass (h,(Intersection (T))) is Element of K10( the carrier of T)
h is Element of the carrier of T
f . h is Element of the carrier of S
EqClass (h,(Intersection (T))) is Element of K10( the carrier of T)
proj (Intersection (T)) is non empty Relation-like the carrier of T -defined Intersection (T) -valued Function-like V14( the carrier of T) V18( the carrier of T, Intersection (T)) Element of K10(K11( the carrier of T,(Intersection (T))))
K11( the carrier of T,(Intersection (T))) is non empty set
K10(K11( the carrier of T,(Intersection (T)))) is non empty set
(T) . h is Element of the carrier of (T)
c₁₂ is Element of the carrier of S
{c₁₂} is Element of K10( the carrier of S)
f " {c₁₂} is Element of K10( the carrier of T)
((T) * (x * y)) . h is set
(x * y) . ((T) . h) is set
x . ((T) . h) is set
y . (x . ((T) . h)) is set
y . (f " {c₁₂}) is set
rng y is set
ty is set
h is set
y . h is set
h is Element of the carrier of S
{h} is Element of K10( the carrier of S)
f " {h} is Element of K10( the carrier of T)
rng (x * y) is set
ty is set
ty is non empty Relation-like the carrier of (T) -defined the carrier of S -valued Function-like V14( the carrier of (T)) V18( the carrier of (T), the carrier of S) Element of K10(K11( the carrier of (T), the carrier of S))
h is non empty Relation-like the carrier of (T) -defined the carrier of S -valued Function-like V14( the carrier of (T)) V18( the carrier of (T), the carrier of S) Element of K10(K11( the carrier of (T), the carrier of S))
h is Element of K10( the carrier of S)
h " h is Element of K10( the carrier of (T))
K10( the carrier of (T)) is non empty set
K10( the carrier of (space (Intersection (T)))) is non empty set
c₁₂ is Element of K10( the carrier of (space (Intersection (T))))
union c₁₂ is set
uhy is set
z2 is set
h * (T) is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of S) Element of K10(K11( the carrier of T, the carrier of S))
(h * (T)) " h is Element of K10( the carrier of T)
(T) " (h " h) is Element of K10( the carrier of T)
uhy is Element of K10( the carrier of T)
h is non empty Relation-like the carrier of (T) -defined the carrier of S -valued Function-like V14( the carrier of (T)) V18( the carrier of (T), the carrier of S) continuous Element of K10(K11( the carrier of (T), the carrier of S))
h * (T) is non empty Relation-like the carrier of T -defined the carrier of T -defined the carrier of S -valued the carrier of S -valued Function-like V14( the carrier of T) V14( the carrier of T) V18( the carrier of T, the carrier of S) V18( the carrier of T, the carrier of S) continuous Element of K10(K11( the carrier of T, the carrier of S))
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
K11( the carrier of T, the carrier of S) is non empty set
K10(K11( the carrier of T, the carrier of S)) is non empty set
(T) is non empty strict TopSpace-like T_0 T_1 TopStruct
(T) is non empty partition-membered Element of K10(K10((bool the carrier of T)))
bool the carrier of T is non empty Element of K10(K10( the carrier of T))
K10( the carrier of T) is non empty set
K10(K10( the carrier of T)) is non empty set
K10((bool the carrier of T)) is non empty set
K10(K10((bool the carrier of T))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of T : b₁ is closed } is set
Intersection (T) is non empty with_non-empty_elements a_partition of the carrier of T
space (Intersection (T)) is non empty strict TopSpace-like TopStruct
the carrier of (T) is non empty set
(S) is non empty strict TopSpace-like T_0 T_1 TopStruct
(S) is non empty partition-membered Element of K10(K10((bool the carrier of S)))
bool the carrier of S is non empty Element of K10(K10( the carrier of S))
K10( the carrier of S) is non empty set
K10(K10( the carrier of S)) is non empty set
K10((bool the carrier of S)) is non empty set
K10(K10((bool the carrier of S))) is non empty set
{ b₁ where b₁ is non empty with_non-empty_elements a_partition of the carrier of S : b₁ is closed } is set
Intersection (S) is non empty with_non-empty_elements a_partition of the carrier of S
space (Intersection (S)) is non empty strict TopSpace-like TopStruct
the carrier of (S) is non empty set
K11( the carrier of (T), the carrier of (S)) is non empty set
K10(K11( the carrier of (T), the carrier of (S))) is non empty set
f is non empty Relation-like the carrier of T -defined the carrier of S -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of S) continuous Element of K10(K11( the carrier of T, the carrier of S))
(S) is non empty Relation-like the carrier of S -defined the carrier of (S) -valued Function-like V14( the carrier of S) V18( the carrier of S, the carrier of (S)) continuous Element of K10(K11( the carrier of S, the carrier of (S)))
K11( the carrier of S, the carrier of (S)) is non empty set
K10(K11( the carrier of S, the carrier of (S))) is non empty set
Proj (Intersection (S)) is non empty Relation-like the carrier of S -defined the carrier of (space (Intersection (S))) -valued Function-like V14( the carrier of S) V18( the carrier of S, the carrier of (space (Intersection (S)))) continuous Element of K10(K11( the carrier of S, the carrier of (space (Intersection (S)))))
the carrier of (space (Intersection (S))) is non empty set
K11( the carrier of S, the carrier of (space (Intersection (S)))) is non empty set
K10(K11( the carrier of S, the carrier of (space (Intersection (S))))) is non empty set
(S) * f is non empty Relation-like the carrier of T -defined the carrier of T -defined the carrier of (S) -valued the carrier of (S) -valued Function-like V14( the carrier of T) V14( the carrier of T) V18( the carrier of T, the carrier of (S)) V18( the carrier of T, the carrier of (S)) continuous Element of K10(K11( the carrier of T, the carrier of (S)))
K11( the carrier of T, the carrier of (S)) is non empty set
K10(K11( the carrier of T, the carrier of (S))) is non empty set
(T) is non empty Relation-like the carrier of T -defined the carrier of (T) -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of (T)) continuous Element of K10(K11( the carrier of T, the carrier of (T)))
K11( the carrier of T, the carrier of (T)) is non empty set
K10(K11( the carrier of T, the carrier of (T))) is non empty set
Proj (Intersection (T)) is non empty Relation-like the carrier of T -defined the carrier of (space (Intersection (T))) -valued Function-like V14( the carrier of T) V18( the carrier of T, the carrier of (space (Intersection (T)))) continuous Element of K10(K11( the carrier of T, the carrier of (space (Intersection (T)))))
the carrier of (space (Intersection (T))) is non empty set
K11( the carrier of T, the carrier of (space (Intersection (T)))) is non empty set
K10(K11( the carrier of T, the carrier of (space (Intersection (T))))) is non empty set
g1 is non empty Relation-like the carrier of (T) -defined the carrier of (S) -valued Function-like V14( the carrier of (T)) V18( the carrier of (T), the carrier of (S)) continuous Element of K10(K11( the carrier of (T), the carrier of (S)))
g1 * (T) is non empty Relation-like the carrier of T -defined the carrier of T -defined the carrier of (S) -valued the carrier of (S) -valued Function-like V14( the carrier of T) V14( the carrier of T) V18( the carrier of T, the carrier of (S)) V18( the carrier of T, the carrier of (S)) continuous Element of K10(K11( the carrier of T, the carrier of (S)))
g2 is non empty Relation-like the carrier of (T) -defined the carrier of (S) -valued Function-like V14( the carrier of (T)) V18( the carrier of (T), the carrier of (S)) continuous Element of K10(K11( the carrier of (T), the carrier of (S)))
g2 * (T) is non empty Relation-like the carrier of T -defined the carrier of T -defined the carrier of (S) -valued the carrier of (S) -valued Function-like V14( the carrier of T) V14( the carrier of T) V18( the carrier of T, the carrier of (S)) V18( the carrier of T, the carrier of (S)) continuous Element of K10(K11( the carrier of T, the carrier of (S)))
x is set
dom g1 is Element of K10( the carrier of (T))
K10( the carrier of (T)) is non empty set
y is Element of the carrier of T
EqClass (y,(Intersection (T))) is Element of K10( the carrier of T)
y is Element of the carrier of T
(T) . y is Element of the carrier of (T)
proj (Intersection (T)) is non empty Relation-like the carrier of T -defined Intersection (T) -valued Function-like V14( the carrier of T) V18( the carrier of T, Intersection (T)) Element of K10(K11( the carrier of T,(Intersection (T))))
K11( the carrier of T,(Intersection (T))) is non empty set
K10(K11( the carrier of T,(Intersection (T)))) is non empty set
dom (T) is Element of K10( the carrier of T)
g2 . x is set
(g2 * (T)) . y is Element of the carrier of (S)
g1 . x is set
dom g2 is Element of K10( the carrier of (T))