:: T_1TOPSP semantic presentation

begin

theorem :: T_1TOPSP:1
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Subset of ) holds (Proj A : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (space b2 : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (space b2 : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (space b2 : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) continuous ) Element of K10(K11( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (space b2 : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) " y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = union y : ( ( ) ( ) Subset of ) : ( ( ) ( ) set ) ;

theorem :: T_1TOPSP:2
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st B : ( ( ) ( ) Subset of ) = union A : ( ( ) ( ) Subset of ) : ( ( ) ( ) set ) holds
( A : ( ( ) ( ) Subset of ) is closed iff B : ( ( ) ( ) Subset of ) is closed ) ;

theorem :: T_1TOPSP:3
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds { A : ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) where A is ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : A : ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) is closed } is ( ( partition-membered ) ( partition-membered ) Part-Family of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func Closed_Partitions T -> ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) equals :: T_1TOPSP:def 1
 { A : ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) where A is ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : A : ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) is closed } ;
end;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func T_1-reflex T -> ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) equals :: T_1TOPSP:def 2
 space (Intersection (Closed_Partitions T : ( ( ) ( ) TopStruct ) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopStruct ) ;
end;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) -> non empty strict TopSpace-like ;
end;

theorem :: T_1TOPSP:4
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) is T_1 ;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) -> TopSpace-like T_1 ;
end;

registration
cluster non empty TopSpace-like T_1 for ( ( ) ( ) TopStruct ) ;
end;

definition
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
func T_1-reflect T -> ( ( Function-like V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) equals :: T_1TOPSP:def 3
 Proj (Intersection (Closed_Partitions T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (space (Intersection (Closed_Partitions T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (space (Intersection (Closed_Partitions T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (space (Intersection (Closed_Partitions T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) continuous ) Element of K10(K11( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (space (Intersection (Closed_Partitions T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: T_1TOPSP:5
for T, T1 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_1 holds
( { (f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " {z : ( ( ) ( ) Subset of ) } : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) where z is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : z : ( ( ) ( ) Subset of ) in rng f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) } is ( ( ) ( non empty with_non-empty_elements ) a_partition of the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) & ( for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) in { (f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " {z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) where z is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in rng f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) } holds
A : ( ( ) ( ) Subset of ) is closed ) ) ;

theorem :: T_1TOPSP:6
for T, T1 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_1 holds
for w being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st w : ( ( ) ( ) set ) = EqClass (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,(Intersection (Closed_Partitions T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( non empty partition-membered ) ( non empty partition-membered ) Part-Family of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty with_non-empty_elements ) a_partition of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
w : ( ( ) ( ) set ) c= f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " {(f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: T_1TOPSP:7
for T, T1 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_1 holds
for w being ( ( ) ( ) set ) st w : ( ( ) ( ) set ) in the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) holds
ex z being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in rng f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & w : ( ( ) ( ) set ) c= f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " {z : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) Element of K10( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K10( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: T_1TOPSP:8
for T, T1 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is T_1 holds
ex h being ( ( Function-like V18( the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = h : ( ( Function-like V18( the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * (T_1-reflect T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Element of K10(K11( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

definition
let T, S be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let f be ( ( Function-like V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
func T_1-reflex f -> ( ( Function-like V18( the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) V18( the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) means :: T_1TOPSP:def 4
(T_1-reflect S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( Function-like V18( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V18( the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( ) ( ) Element of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( Function-like ) ( Relation-like the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K10(K11( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = it : ( ( ) ( ) Element of the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) * (T_1-reflect T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( Function-like V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) ( non empty Relation-like the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V14( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V18( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) continuous ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of K10(K11( the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of (T_1-reflex S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;