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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

{c

f " {c

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

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

union c

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

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

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