:: WAYBEL18 semantic presentation

begin

theorem :: WAYBEL18:1
for X being ( ( ) ( ) set )
for A, B being ( ( ) ( ) Subset-Family of ) st ( B : ( ( ) ( ) Subset-Family of ) = A : ( ( ) ( ) Subset-Family of ) \ {{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19(K19(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) or A : ( ( ) ( ) Subset-Family of ) = B : ( ( ) ( ) Subset-Family of ) \/ {{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
UniCl A : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K19(K19(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = UniCl B : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of K19(K19(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL18:2
for T being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for K being ( ( ) ( ) Subset-Family of ) holds
( K : ( ( ) ( ) Subset-Family of ) is ( ( open quasi_basis ) ( open quasi_basis ) Basis of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) iff K : ( ( ) ( ) Subset-Family of ) \ {{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) } : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19(K19( the carrier of b1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( open quasi_basis ) ( open quasi_basis ) Basis of T : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ) ;

definition
let F be ( ( Relation-like ) ( Relation-like ) Relation) ;
attr F is TopStruct-yielding means :: WAYBEL18:def 1
 for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in rng F : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) TopStruct ) ;
end;

registration
cluster Relation-like Function-like TopStruct-yielding -> Relation-like Function-like 1-sorted-yielding for ( ( ) ( ) set ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like total TopStruct-yielding for ( ( ) ( ) set ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
cluster Relation-like I : ( ( ) ( ) set ) -defined Function-like total non-Empty TopStruct-yielding for ( ( ) ( ) set ) ;
end;

definition
let J be ( ( non empty ) ( non empty ) set ) ;
let A be ( ( Relation-like J : ( ( non empty ) ( non empty ) set ) -defined Function-like total TopStruct-yielding ) ( Relation-like J : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding TopStruct-yielding ) ManySortedSet of J : ( ( non empty ) ( non empty ) set ) ) ;
let j be ( ( ) ( ) Element of J : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func A . j -> ( ( ) ( ) TopStruct ) ;
end;

definition
let I be ( ( ) ( ) set ) ;
let J be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding TopStruct-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
func product_prebasis J -> ( ( ) ( ) Subset-Family of ) means :: WAYBEL18:def 2
 for x being ( ( ) ( with_common_domain ) Subset of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( with_common_domain ) Subset of ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) Element of K19(K19(I : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) iff ex i being ( ( ) ( ) set ) ex T being ( ( ) ( ) TopStruct ) ex V being ( ( ) ( ) Subset of ) st
( i : ( ( ) ( ) set ) in I : ( ( ) ( ) set ) & V : ( ( ) ( ) Subset of ) is open & T : ( ( ) ( ) TopStruct ) = J : ( ( ) ( ) set ) . i : ( ( ) ( ) set ) : ( ( ) ( ) set ) & x : ( ( ) ( with_common_domain ) Subset of ( ( ) ( non empty ) set ) ) = product ((Carrier J : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) +* (i : ( ( ) ( ) set ) ,V : ( ( ) ( ) Subset of ) )) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) ) );
end;

theorem :: WAYBEL18:3
for X being ( ( ) ( ) set )
for A being ( ( ) ( ) Subset-Family of ) holds TopStruct(# X : ( ( ) ( ) set ) ,(UniCl (FinMeetCl A : ( ( ) ( ) Subset-Family of ) ) : ( ( ) ( ) Element of K19(K19(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K19(K19(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) is TopSpace-like ;

definition
let I be ( ( ) ( ) set ) ;
let J be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
func product J -> ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopSpace) means :: WAYBEL18:def 3
( the carrier of it : ( ( ) ( ) Element of K19(K19(I : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = product (Carrier J : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) & product_prebasis J : ( ( ) ( ) set ) : ( ( ) ( ) Subset-Family of ) is ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of it : ( ( ) ( ) Element of K19(K19(I : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) );
end;

registration
let I be ( ( ) ( ) set ) ;
let J be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster product J : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) set ) : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopSpace) -> non empty strict TopSpace-like ;
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let J be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
let i be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func J . i -> ( ( non empty ) ( non empty ) TopStruct ) ;
end;

registration
let I be ( ( ) ( ) set ) ;
let J be ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( ) ( ) set ) ) ;
cluster product J : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) set ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopSpace) -> strict TopSpace-like constituted-Functions ;
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let J be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
let x be ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) ;
let i be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func x . i -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
end;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let J be ( ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) ;
let i be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
func proj (J,i) -> ( ( Function-like quasi_total ) ( Relation-like the carrier of (product J : ( ( ) ( ) set ) ) : ( ( strict TopSpace-like ) ( strict TopSpace-like ) TopSpace) : ( ( ) ( ) set ) -defined the carrier of (J : ( ( ) ( ) set ) . i : ( ( ) ( ) Element of K19(K19(I : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) equals :: WAYBEL18:def 4
 proj ((Carrier J : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) ,i : ( ( ) ( ) Element of K19(K19(I : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like product (Carrier J : ( ( ) ( ) set ) ) : ( ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like total ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) -defined Function-like total ) set ) ;
end;

theorem :: WAYBEL18:4
for I being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) )
for P being ( ( ) ( ) Subset of ) holds (proj (J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (product b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of (product b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = product ((Carrier J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) set ) +* (i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,P : ( ( ) ( ) Subset of ) )) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( functional with_common_domain product-like ) set ) ;

theorem :: WAYBEL18:5
for I being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds proj (J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (product b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b3 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

theorem :: WAYBEL18:6
for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for I being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (product b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (product b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous iff for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds (proj (J : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of (product b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (product b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (b3 : ( ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b2 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b2 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is continuous ) ;

begin

definition
let Z be ( ( ) ( ) TopStruct ) ;
attr Z is injective means :: WAYBEL18:def 5
 for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is continuous holds
for Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) SubSpace of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds
ex g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st
( g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is continuous & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) | the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued the carrier of Z : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like ) Element of K19(K20( the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of Z : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of Z : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) );
end;

theorem :: WAYBEL18:7
for I being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of I : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) holds J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( non empty ) ( non empty ) TopStruct ) is injective ) holds
product J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total 1-sorted-yielding non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) is injective ;

theorem :: WAYBEL18:8
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is injective holds
for S being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st S : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is_a_retract_of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds
S : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) is injective ;

definition
let X be ( ( ) ( ) 1-sorted ) ;
let Y be ( ( ) ( ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ;
func Image f -> ( ( ) ( ) SubSpace of Y : ( ( ) ( ) set ) ) equals :: WAYBEL18:def 6
Y : ( ( ) ( ) set ) | (rng f : ( ( ) ( ) Element of K19(K19(X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K19( the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( strict ) SubSpace of Y : ( ( ) ( ) set ) ) ;
end;

registration
let X be ( ( non empty ) ( non empty ) 1-sorted ) ;
let Y be ( ( non empty ) ( non empty ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster Image f : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of X : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) SubSpace of Y : ( ( non empty ) ( non empty ) TopStruct ) ) -> non empty ;
end;

theorem :: WAYBEL18:9
for X being ( ( ) ( ) 1-sorted )
for Y being ( ( ) ( ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) holds the carrier of (Image f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) ) : ( ( ) ( ) SubSpace of b2 : ( ( ) ( ) TopStruct ) ) : ( ( ) ( ) set ) = rng f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

definition
let X be ( ( ) ( ) 1-sorted ) ;
let Y be ( ( non empty ) ( non empty ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;
func corestr f -> ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of (Image f : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) SubSpace of Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) equals :: WAYBEL18:def 7
f : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20( the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL18:10
for X, Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( 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 quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( 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 quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
corestr f : ( ( Function-like quasi_total ) ( 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 quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b3 : ( ( Function-like quasi_total ) ( 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 quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) is continuous ;

registration
let X be ( ( ) ( ) 1-sorted ) ;
let Y be ( ( non empty ) ( non empty ) TopStruct ) ;
let f be ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster corestr f : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of K19(K20( the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of (Image f : ( ( Function-like quasi_total ) ( Relation-like the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Element of K19(K20( the carrier of X : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) SubSpace of Y : ( ( non empty ) ( non empty ) TopStruct ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) -> Function-like quasi_total onto ;
end;

definition
let X, Y be ( ( ) ( ) TopStruct ) ;
pred X is_Retract_of Y means :: WAYBEL18:def 8
 ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is continuous & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like ) Element of K19(K20( the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) & Image f : ( ( Function-like quasi_total ) ( Relation-like the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of Y : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( ) SubSpace of Y : ( ( ) ( ) set ) ) ,X : ( ( ) ( ) set ) are_homeomorphic );
end;

theorem :: WAYBEL18:11
for T, S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is injective holds
for f being ( ( Function-like quasi_total ) ( 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 non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st corestr f : ( ( Function-like quasi_total ) ( 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 non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b3 : ( ( Function-like quasi_total ) ( 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 non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total onto ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is_Retract_of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;

definition
func Sierpinski_Space -> ( ( strict ) ( strict ) TopStruct ) means :: WAYBEL18:def 9
( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = {0 : ( ( ) ( Relation-like non-empty empty-yielding empty ) Element of K108() : ( ( ) ( non finite countable denumerable ) Element of K19(K104() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) & the topology of it : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(K19( the carrier of it : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) ,{0 : ( ( ) ( Relation-like non-empty empty-yielding empty ) Element of K108() : ( ( ) ( non finite countable denumerable ) Element of K19(K104() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) );
end;

registration
cluster Sierpinski_Space : ( ( strict ) ( strict ) TopStruct ) -> non empty strict TopSpace-like ;
end;

registration
cluster Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) -> strict T_0 ;
end;

registration
cluster Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 ) TopStruct ) -> strict injective ;
end;

registration
let I be ( ( ) ( ) set ) ;
let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
cluster I : ( ( ) ( ) set ) --> S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like constant total ) set ) -> non-Empty ;
end;

registration
let I be ( ( ) ( ) set ) ;
let T be ( ( ) ( ) TopStruct ) ;
cluster I : ( ( ) ( ) set ) --> T : ( ( ) ( ) TopStruct ) : ( ( ) ( Relation-like I : ( ( ) ( ) set ) -defined Function-like constant total ) set ) -> TopStruct-yielding ;
end;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let L be ( ( non empty antisymmetric ) ( non empty antisymmetric ) RelStr ) ;
cluster product (I : ( ( non empty ) ( non empty ) set ) --> L : ( ( non empty antisymmetric ) ( non empty antisymmetric ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined {L : ( ( non empty antisymmetric ) ( non empty antisymmetric ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty ) Element of K19(K20(I : ( ( non empty ) ( non empty ) set ) ,{L : ( ( non empty antisymmetric ) ( non empty antisymmetric ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict constituted-Functions ) RelStr ) -> strict antisymmetric ;
end;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let L be ( ( non empty transitive ) ( non empty transitive ) RelStr ) ;
cluster product (I : ( ( non empty ) ( non empty ) set ) --> L : ( ( non empty transitive ) ( non empty transitive ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined {L : ( ( non empty transitive ) ( non empty transitive ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty ) Element of K19(K20(I : ( ( non empty ) ( non empty ) set ) ,{L : ( ( non empty transitive ) ( non empty transitive ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict constituted-Functions ) RelStr ) -> strict transitive ;
end;

theorem :: WAYBEL18:12
for T being ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of BoolePoset 1 : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) holds the topology of T : ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of BoolePoset 1 : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of BoolePoset 1 : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL18:13
for I being ( ( non empty ) ( non empty ) set ) holds { (product ((Carrier (I : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like total ) set ) +* (i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ,{1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) )) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( functional with_common_domain product-like ) set ) where i is ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) : verum } is ( ( open quasi_prebasis ) ( open quasi_prebasis ) prebasis of product (I : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) ) ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete ) LATTICE) ;
cluster product (I : ( ( non empty ) ( non empty ) set ) --> L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined {L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(I : ( ( non empty ) ( non empty ) set ) ,{L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric constituted-Functions ) RelStr ) -> strict with_suprema complete ;
end;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let X be ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) LATTICE) ;
cluster product (I : ( ( non empty ) ( non empty ) set ) --> X : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like I : ( ( non empty ) ( non empty ) set ) -defined {X : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(I : ( ( non empty ) ( non empty ) set ) ,{X : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() up-complete /\-complete ) RelStr ) -> strict algebraic ;
end;

theorem :: WAYBEL18:14
for X being ( ( non empty ) ( non empty ) set ) ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of (BoolePoset b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (BoolePoset b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic & ( for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( Relation-like the carrier of (BoolePoset b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = chi (Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ,X : ( ( non empty ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL18:15
for I being ( ( non empty ) ( non empty ) set )
for T being ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of product (I : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) holds the topology of T : ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of product (b1 : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b2 : ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of product (b1 : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of (product (I : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) Element of K19(K19( the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL18:16
for T, S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st 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 ) & the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is injective holds
S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is injective ;

theorem :: WAYBEL18:17
for I being ( ( non empty ) ( non empty ) set )
for T being ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of product (I : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) holds T : ( ( Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() up-complete /\-complete Scott ) TopAugmentation of product (b1 : ( ( non empty ) ( non empty ) set ) --> (BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding RelStr-yielding non-Empty reflexive-yielding ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,{(BoolePoset 1 : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete constituted-Functions lower-bounded upper-bounded V251() satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic up-complete /\-complete ) RelStr ) ) is injective ;

theorem :: WAYBEL18:18
for T being ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) ex M being ( ( non empty ) ( non empty ) set ) ex f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (product (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st corestr f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (product (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b3 : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (product (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of product (b2 : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total onto ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

theorem :: WAYBEL18:19
for T being ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) st T : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) is injective holds
ex M being ( ( non empty ) ( non empty ) set ) st T : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) is_Retract_of product (M : ( ( non empty ) ( non empty ) set ) --> Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined {Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) -valued Function-like constant non empty total quasi_total 1-sorted-yielding non-Empty TopStruct-yielding ) Element of K19(K20(b2 : ( ( non empty ) ( non empty ) set ) ,{Sierpinski_Space : ( ( strict ) ( non empty strict TopSpace-like T_0 injective ) TopStruct ) } : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopSpace) ;