:: YELLOW14 semantic presentation

begin

theorem :: YELLOW14:1
bool 1 : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K6(K6(1 : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {0 : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) Element of K126() : ( ( ) ( ) Element of K6(K122() : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty ) set ) } : ( ( ) ( non empty finite ) set ) ;

theorem :: YELLOW14:2
for X being ( ( ) ( ) set )
for Y being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds rng ((id X : ( ( ) ( ) set ) ) : ( ( V18(b1 : ( ( ) ( ) set ) ) ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like one-to-one V18(b1 : ( ( ) ( ) set ) ) quasi_total ) Element of K6(K7(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) | Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b2 : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) -defined b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like ) Element of K6(K7(b1 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:3
for S being ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted )
for T being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) , ( ( ) ( ) set ) ) st rng f : ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() with_non-empty_elements ) Element of K6( the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( ) ( ) 1-sorted ) : ( ( ) ( non proper ) Element of K6( the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) holds
T : ( ( ) ( ) 1-sorted ) is empty ;

theorem :: YELLOW14:4
for S being ( ( ) ( ) 1-sorted )
for T being ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( ) set ) , ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) ) st dom f : ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( empty ) ( empty trivial finite {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -element ) 1-sorted ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( ) set ) , ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) set ) ) : ( ( ) ( empty trivial non proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) Element of K6( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty finite V38() ) set ) ) = [#] S : ( ( ) ( ) 1-sorted ) : ( ( ) ( empty trivial non proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) Element of K6( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty finite V38() ) set ) ) holds
S : ( ( ) ( ) 1-sorted ) is empty ;

theorem :: YELLOW14:5
for S being ( ( non empty ) ( non empty ) 1-sorted )
for T being ( ( ) ( ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) st dom f : ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( empty trivial non proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() ) Element of K6( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty finite V38() ) set ) ) = [#] S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty finite V38() ) set ) ) holds
not T : ( ( ) ( ) 1-sorted ) is empty ;

theorem :: YELLOW14:6
for S being ( ( ) ( ) 1-sorted )
for T being ( ( non empty ) ( non empty ) 1-sorted )
for f being ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st rng f : ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one constant functional V18( the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) quasi_total Function-yielding V33() finite finite-yielding V38() ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) : ( ( ) ( empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V33() finite finite-yielding V38() with_non-empty_elements ) Element of K6( the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty non proper ) Element of K6( the carrier of b2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
not S : ( ( ) ( ) 1-sorted ) is empty ;

definition
let S be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
let T be ( ( non empty ) ( non empty ) RelStr ) ;
let f be ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of S : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of T : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of S : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
redefine attr f is directed-sups-preserving means :: YELLOW14:def 1
 for X being ( ( non empty directed ) ( non empty directed ) Subset of ) holds f : ( ( ) ( ) Element of K6(K6(S : ( ( ) ( ) TopRelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) preserves_sup_of X : ( ( non empty directed ) ( non empty directed ) Subset of ) ;
end;

definition
let R be ( ( ) ( ) 1-sorted ) ;
let N be ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ;
attr N is Function-yielding means :: YELLOW14:def 2
 the mapping of N : ( ( ) ( ) NetStr over R : ( ( ) ( ) TopRelStr ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of N : ( ( ) ( ) NetStr over R : ( ( ) ( ) TopRelStr ) ) : ( ( ) ( ) set ) -defined the carrier of R : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K6(K7( the carrier of N : ( ( ) ( ) NetStr over R : ( ( ) ( ) TopRelStr ) ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) is Function-yielding ;
end;

registration
cluster non empty constituted-Functions for ( ( ) ( ) 1-sorted ) ;
end;

registration
cluster non empty strict constituted-Functions for ( ( ) ( ) RelStr ) ;
end;

registration
let R be ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ;
cluster -> Function-yielding for ( ( ) ( ) NetStr over R : ( ( ) ( ) TopRelStr ) ) ;
end;

registration
let R be ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ;
cluster strict Function-yielding for ( ( ) ( ) NetStr over R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ) ;
end;

registration
let R be ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) ;
cluster non empty strict Function-yielding for ( ( ) ( ) NetStr over R : ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) ) ;
end;

registration
let R be ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ;
let N be ( ( Function-yielding ) ( Function-yielding ) NetStr over R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ) ;
cluster the mapping of N : ( ( Function-yielding ) ( Function-yielding ) NetStr over R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of N : ( ( Function-yielding ) ( Function-yielding ) NetStr over R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of K6(K7( the carrier of N : ( ( Function-yielding ) ( Function-yielding ) NetStr over R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of R : ( ( constituted-Functions ) ( constituted-Functions ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) -> Function-like quasi_total Function-yielding ;
end;

registration
let R be ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) ;
cluster non empty transitive strict directed Function-yielding for ( ( ) ( ) NetStr over R : ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) ) ;
end;

registration
let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
cluster rng the mapping of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -> non empty ;
end;

registration
let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let N be ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ;
cluster rng (netmap (N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) ,S : ( ( non empty ) ( non empty ) 1-sorted ) )) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of N : ( ( non empty ) ( non empty ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) -> non empty ;
end;

theorem :: YELLOW14:7
for A, B, C being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g, h being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is monotone holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * g : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) <= f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * h : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:8
for S being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopRelStr )
for f, g being ( ( Function-like quasi_total ) ( 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 ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for x, y being ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( 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 ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) & y : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) = g : ( ( Function-like quasi_total ) ( 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 ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) iff f : ( ( Function-like quasi_total ) ( 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 ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) <= g : ( ( Function-like quasi_total ) ( 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 ) TopRelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) ;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let R be ( ( non empty ) ( non empty ) RelStr ) ;
let f be ( ( ) ( Relation-like Function-like ) Element of ( ( ) ( non empty ) set ) ) ;
let i be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func f . i -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

begin

theorem :: YELLOW14:9
for S, T being ( ( ) ( ) RelStr )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is isomorphic holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) is onto ;

registration
let S, T be ( ( ) ( ) RelStr ) ;
cluster Function-like quasi_total isomorphic -> Function-like quasi_total onto for ( ( ) ( ) Element of K6(K7( the carrier of S : ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty ) ( non empty ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: YELLOW14:10
for S, T being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) /" : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) is isomorphic ;

theorem :: YELLOW14:11
for S, T being ( ( non empty ) ( non empty ) RelStr ) st S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) are_isomorphic & S : ( ( non empty ) ( non empty ) RelStr ) is with_infima holds
T : ( ( non empty ) ( non empty ) RelStr ) is with_infima ;

theorem :: YELLOW14:12
for S, T being ( ( non empty ) ( non empty ) RelStr ) st S : ( ( non empty ) ( non empty ) RelStr ) ,T : ( ( non empty ) ( non empty ) RelStr ) are_isomorphic & S : ( ( non empty ) ( non empty ) RelStr ) is with_suprema holds
T : ( ( non empty ) ( non empty ) RelStr ) is with_suprema ;

theorem :: YELLOW14:13
for L being ( ( ) ( ) RelStr ) st L : ( ( ) ( ) RelStr ) is empty holds
L : ( ( ) ( ) RelStr ) is bounded ;

registration
cluster empty -> bounded for ( ( ) ( ) RelStr ) ;
end;

theorem :: YELLOW14:14
for S, T being ( ( ) ( ) RelStr ) st S : ( ( ) ( ) RelStr ) ,T : ( ( ) ( ) RelStr ) are_isomorphic & S : ( ( ) ( ) RelStr ) is lower-bounded holds
T : ( ( ) ( ) RelStr ) is lower-bounded ;

theorem :: YELLOW14:15
for S, T being ( ( ) ( ) RelStr ) st S : ( ( ) ( ) RelStr ) ,T : ( ( ) ( ) RelStr ) are_isomorphic & S : ( ( ) ( ) RelStr ) is upper-bounded holds
T : ( ( ) ( ) RelStr ) is upper-bounded ;

theorem :: YELLOW14:16
for S, T being ( ( non empty ) ( non empty ) RelStr )
for A being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic & ex_sup_of A : ( ( ) ( ) Subset of ) ,S : ( ( non empty ) ( non empty ) RelStr ) holds
ex_sup_of f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,T : ( ( non empty ) ( non empty ) RelStr ) ;

theorem :: YELLOW14:17
for S, T being ( ( non empty ) ( non empty ) RelStr )
for A being ( ( ) ( ) Subset of )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic & ex_inf_of A : ( ( ) ( ) Subset of ) ,S : ( ( non empty ) ( non empty ) RelStr ) holds
ex_inf_of f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,T : ( ( non empty ) ( non empty ) RelStr ) ;

begin

theorem :: YELLOW14:18
for S, T being ( ( ) ( ) TopStruct ) st ( S : ( ( ) ( ) TopStruct ) ,T : ( ( ) ( ) TopStruct ) are_homeomorphic or ex f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) st
( dom f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = [#] S : ( ( ) ( ) TopStruct ) : ( ( ) ( non empty non proper dense ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & rng f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) -valued Function-like V18( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) quasi_total ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of K6( the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = [#] T : ( ( ) ( ) TopStruct ) : ( ( ) ( non empty non proper dense ) Element of K6( the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) holds
( S : ( ( ) ( ) TopStruct ) is empty iff T : ( ( ) ( ) TopStruct ) is empty ) ;

theorem :: YELLOW14:19
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) holds T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) , TopStruct(# the carrier of T : ( ( 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 K6(K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) are_homeomorphic ;

registration
let T be ( ( non empty reflexive Scott ) ( non empty reflexive Scott ) TopRelStr ) ;
cluster open -> upper inaccessible for ( ( ) ( ) Element of K6( the carrier of T : ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
cluster upper inaccessible -> open for ( ( ) ( ) Element of K6( the carrier of T : ( ( non empty constituted-Functions ) ( non empty constituted-Functions ) 1-sorted ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: YELLOW14:20
for T being ( ( ) ( ) TopStruct )
for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite ) set ) & Cl X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= Cl Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in Cl Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:21
for T being ( ( ) ( ) TopStruct )
for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for Y, V being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) = {y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite ) set ) & x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in Cl Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) & V : ( ( ) ( ) Subset of ) is open & x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) holds
y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) ;

theorem :: YELLOW14:22
for T being ( ( ) ( ) TopStruct )
for x, y being ( ( ) ( ) Point of ( ( ) ( ) set ) )
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = {x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite ) set ) & Y : ( ( ) ( ) Subset of ) = {y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non empty finite ) set ) & ( for V being ( ( ) ( ) Subset of ) st V : ( ( ) ( ) Subset of ) is open & x : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) holds
y : ( ( ) ( ) Point of ( ( ) ( ) set ) ) in V : ( ( ) ( ) Subset of ) ) holds
Cl X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) c= Cl Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:23
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for A being ( ( irreducible ) ( non empty irreducible ) Subset of )
for B being ( ( ) ( ) Subset of ) st A : ( ( irreducible ) ( non empty irreducible ) Subset of ) = B : ( ( ) ( ) Subset of ) & TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K6(K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( 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 K6(K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) holds
B : ( ( ) ( ) Subset of ) is irreducible ;

theorem :: YELLOW14:24
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for a being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for b being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) & TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K6(K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( 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 K6(K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & a : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_dense_point_of A : ( ( ) ( ) Subset of ) holds
b : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) is_dense_point_of B : ( ( ) ( ) Subset of ) ;

theorem :: YELLOW14:25
for S, T being ( ( ) ( ) TopStruct )
for A being ( ( ) ( ) Subset of )
for B being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = B : ( ( ) ( ) Subset of ) & TopStruct(# the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) = TopStruct(# the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) & A : ( ( ) ( ) Subset of ) is compact holds
B : ( ( ) ( ) Subset of ) is compact ;

theorem :: YELLOW14:26
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K6(K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( 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 K6(K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is sober holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is sober ;

theorem :: YELLOW14:27
for S, T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TopStruct(# the carrier of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of K6(K6( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of T : ( ( 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 K6(K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & S : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally-compact holds
T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is locally-compact ;

theorem :: YELLOW14:28
for S, T being ( ( ) ( ) TopStruct ) st TopStruct(# the carrier of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of S : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of b1 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) TopStruct ) = TopStruct(# the carrier of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) , the topology of T : ( ( ) ( ) TopStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of b2 : ( ( ) ( ) TopStruct ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) & S : ( ( ) ( ) TopStruct ) is compact holds
T : ( ( ) ( ) TopStruct ) is compact ;

definition
let I be ( ( non empty ) ( non empty ) set ) ;
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let x be ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) ;
let i be ( ( ) ( ) Element of I : ( ( non empty ) ( non empty ) set ) ) ;
:: original: .
redefine func x . i -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;
end;

theorem :: YELLOW14:29
for M being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of M : ( ( non empty ) ( non empty ) set ) )
for x, y being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) in Cl {y : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty functional finite ) Element of K6( the carrier of (product b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty closed ) Element of K6( the carrier of (product b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) iff for i being ( ( ) ( ) Element of M : ( ( non empty ) ( non empty ) set ) ) holds x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) in Cl {(y : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K6( the carrier of (b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (b2 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b5 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW14:30
for M being ( ( non empty ) ( non empty ) set )
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x, y being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) in Cl {y : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty functional finite ) Element of K6( the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like constant V18(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V365() non-Empty TopStruct-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,{b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty closed ) Element of K6( the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like constant V18(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V365() non-Empty TopStruct-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,{b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) iff for i being ( ( ) ( ) Element of M : ( ( non empty ) ( non empty ) set ) ) holds x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in Cl {(y : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty closed ) Element of K6( the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: YELLOW14:31
for M being ( ( non empty ) ( non empty ) set )
for i being ( ( ) ( ) Element of M : ( ( non empty ) ( non empty ) set ) )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of M : ( ( non empty ) ( non empty ) set ) )
for x being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) holds pi ((Cl {x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty functional finite ) Element of K6( the carrier of (product b3 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty closed ) Element of K6( the carrier of (product b3 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = Cl {(x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of (b3 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K6( the carrier of (b3 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K6( the carrier of (b3 : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) . b2 : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:32
for M being ( ( non empty ) ( non empty ) set )
for i being ( ( ) ( ) Element of M : ( ( non empty ) ( non empty ) set ) )
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x being ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) holds pi ((Cl {x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty functional finite ) Element of K6( the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like constant V18(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V365() non-Empty TopStruct-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,{b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty closed ) Element of K6( the carrier of (product (b1 : ( ( non empty ) ( non empty ) set ) --> b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( non empty Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined {b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) -valued Function-like constant V18(b1 : ( ( non empty ) ( non empty ) set ) ) quasi_total V365() non-Empty TopStruct-yielding ) Element of K6(K7(b1 : ( ( non empty ) ( non empty ) set ) ,{b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) = Cl {(x : ( ( ) ( Relation-like Function-like ) Point of ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K6( the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty closed ) Element of K6( the carrier of b3 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:33
for X, Y being ( ( non empty ) ( non empty ) TopStruct )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( 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 ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = id X : ( ( non empty ) ( non empty ) TopStruct ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one V18( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism open ) Element of K6(K7( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = id X : ( ( non empty ) ( non empty ) TopStruct ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one V18( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism open ) Element of K6(K7( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) & f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous & g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous holds
TopStruct(# the carrier of X : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the topology of X : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of b1 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) = TopStruct(# the carrier of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) , the topology of Y : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( ) Element of K6(K6( the carrier of b2 : ( ( non empty ) ( non empty ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) TopStruct ) ;

theorem :: YELLOW14:34
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 V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) 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 V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) 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 V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) 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 V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total onto ) Element of K6(K7( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , 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 V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) 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 ) ) : ( ( ) ( Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) is continuous 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 b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

registration
let X be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
let Y be ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ;
cluster incl Y : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of Y : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) -defined the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of Y : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of Y : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of X : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) -> Function-like quasi_total continuous ;
end;

theorem :: YELLOW14:35
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) 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 b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds
(corestr f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total onto ) Element of K6(K7( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) * (incl (Image f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of K6(K7( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty Relation-like the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K6(K7( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) = id (Image f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one V18( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total onto bijective continuous being_homeomorphism open ) Element of K6(K7( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: YELLOW14:36
for Y being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for W being ( ( non empty ) ( non empty TopSpace-like ) SubSpace of Y : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) holds corestr (incl W : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of K6(K7( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of (Image (incl b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of K6(K7( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total onto ) Element of K6(K7( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of (Image (incl b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) quasi_total continuous ) Element of K6(K7( the carrier of b2 : ( ( non empty ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty TopSpace-like ) SubSpace of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) is being_homeomorphism ;

theorem :: YELLOW14:37
for M being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of M : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( ) ( ) Element of M : ( ( non empty ) ( non empty ) set ) ) holds J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() 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 ( ( TopSpace-like T_0 ) ( TopSpace-like T_0 ) TopSpace) ) holds
product J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) is T_0 ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let T be ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopSpace) ;
cluster product (I : ( ( non empty ) ( non empty ) set ) --> T : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined {T : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like constant V18(I : ( ( non empty ) ( non empty ) set ) ) quasi_total V365() non-Empty TopStruct-yielding ) Element of K6(K7(I : ( ( non empty ) ( non empty ) set ) ,{T : ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) TopStruct ) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) -> strict TopSpace-like T_0 ;
end;

theorem :: YELLOW14:38
for M being ( ( non empty ) ( non empty ) set )
for J being ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of M : ( ( non empty ) ( non empty ) set ) ) st ( for i being ( ( ) ( ) Element of M : ( ( non empty ) ( non empty ) set ) ) holds
( J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() 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 T_1 & J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() 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 TopSpace-like ) ) holds
product J : ( ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) non-Empty TopStruct-yielding ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ) V365() non-Empty TopStruct-yielding ) ManySortedSet of b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like constituted-Functions ) TopStruct ) is T_1 ;

registration
let I be ( ( non empty ) ( non empty ) set ) ;
let T be ( ( non empty TopSpace-like T_1 ) ( non empty TopSpace-like T_0 T_1 ) TopSpace) ;
cluster product (I : ( ( non empty ) ( non empty ) set ) --> T : ( ( non empty TopSpace-like T_1 ) ( non empty TopSpace-like T_0 T_1 ) TopStruct ) ) : ( ( Function-like quasi_total ) ( non empty Relation-like I : ( ( non empty ) ( non empty ) set ) -defined {T : ( ( non empty TopSpace-like T_1 ) ( non empty TopSpace-like T_0 T_1 ) TopStruct ) } : ( ( ) ( non empty finite ) set ) -valued Function-like constant V18(I : ( ( non empty ) ( non empty ) set ) ) quasi_total V365() non-Empty TopStruct-yielding ) Element of K6(K7(I : ( ( non empty ) ( non empty ) set ) ,{T : ( ( non empty TopSpace-like T_1 ) ( non empty TopSpace-like T_0 T_1 ) TopStruct ) } : ( ( ) ( non empty finite ) set ) ) : ( ( ) ( non empty Relation-like ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like T_0 constituted-Functions ) TopStruct ) -> strict TopSpace-like T_1 ;
end;