:: YELLOW14 semantic presentation

begin

theorem :: YELLOW14:1
bool 1 = {0,1} by CARD_1:49, ZFMISC_1:24;

theorem Th2: :: YELLOW14:2
for X being set
for Y being Subset of X holds rng ((id X) | Y) = Y
proof
let X be set ; ::_thesis: for Y being Subset of X holds rng ((id X) | Y) = Y
let Y be Subset of X; ::_thesis: rng ((id X) | Y) = Y
set f = id X;
A1: (id X) | Y is Function of Y,X by FUNCT_2:32;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Y c= rng ((id X) | Y)
let y be set ; ::_thesis: ( y in rng ((id X) | Y) implies y in Y )
assume  y in rng ((id X) | Y) ; ::_thesis: y in Y
then consider x being set  such that
A2: x in dom ((id X) | Y) and
A3: y = ((id X) | Y) . x by FUNCT_1:def_3;
((id X) | Y) . x = (id X) . x by A2, FUNCT_1:47
.= x by A2, FUNCT_1:17 ;
hence  y in Y by A1, A2, A3, FUNCT_2:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng ((id X) | Y) )
 ( X = {} implies Y = {} ) ;
then A4: dom ((id X) | Y) = Y by A1, FUNCT_2:def_1;
assume A5: y in Y ; ::_thesis: y in rng ((id X) | Y)
then ((id X) | Y) . y = (id X) . y by FUNCT_1:49
.= y by A5, FUNCT_1:18 ;
hence  y in rng ((id X) | Y) by A4, A5, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: YELLOW14:3
for S being empty 1-sorted
for T being 1-sorted
for f being Function of S,T st rng f = [#] T holds
T is empty ;

theorem :: YELLOW14:4
for S being 1-sorted
for T being empty 1-sorted
for f being Function of S,T st dom f = [#] S holds
S is empty ;

theorem :: YELLOW14:5
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T st dom f = [#] S holds
not T is empty ;

theorem :: YELLOW14:6
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st rng f = [#] T holds
not S is empty ;

definition
let S be non empty reflexive RelStr ;
let T be non empty RelStr ;
let f be Function of S,T;
redefine attr f is directed-sups-preserving  means :: YELLOW14:def 1
 for X being non empty directed Subset of S holds f preserves_sup_of X;
compatibility
 ( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X )
proof
thus  ( f is directed-sups-preserving implies for X being non empty directed Subset of S holds f preserves_sup_of X ) by WAYBEL_0:def_37; ::_thesis: ( ( for X being non empty directed Subset of S holds f preserves_sup_of X ) implies f is directed-sups-preserving )
assume A1: for X being non empty directed Subset of S holds f preserves_sup_of X ; ::_thesis: f is directed-sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or f preserves_sup_of X )
thus  ( X is empty or not X is directed or f preserves_sup_of X ) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines directed-sups-preserving YELLOW14:def_1_:_
 for S being non empty reflexive RelStr
for T being non empty RelStr
for f being Function of S,T holds
( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X );

definition
let R be 1-sorted ;
let N be NetStr over R;
attrN is Function-yielding  means :Def2: :: YELLOW14:def 2
 the mapping of N is Function-yielding ;
end;

:: deftheorem Def2 defines Function-yielding YELLOW14:def_2_:_
 for R being 1-sorted
for N being NetStr over R holds
( N is Function-yielding iff the mapping of N is Function-yielding );

registration
cluster non empty constituted-Functions for 1-sorted ;
existence
 ex b1 being 1-sorted st
( not b1 is empty & b1 is constituted-Functions )
proof
take A = 1-sorted(# {{}} #); ::_thesis: ( not A is empty & A is constituted-Functions )
thus  not the carrier of A is empty ; :: according to STRUCT_0:def_1 ::_thesis: A is constituted-Functions
let a be Element of A; :: according to MONOID_0:def_1 ::_thesis: a is set
thus  a is set ; ::_thesis: verum
end;
end;

registration
cluster non empty strict constituted-Functions for RelStr ;
existence
 ex b1 being RelStr st
( b1 is strict & not b1 is empty & b1 is constituted-Functions )
proof
take A = RelStr(# {{}},(id {{}}) #); ::_thesis: ( A is strict & not A is empty & A is constituted-Functions )
thus  ( A is strict & not A is empty ) ; ::_thesis: A is constituted-Functions
let a be Element of A; :: according to MONOID_0:def_1 ::_thesis: a is set
thus  a is set ; ::_thesis: verum
end;
end;

registration
let R be constituted-Functions 1-sorted ;
cluster  ->  Function-yielding for NetStr over R;
coherence
 for b1 being NetStr over R holds b1 is Function-yielding
proof
let N be NetStr over R; ::_thesis: N is Function-yielding
let x be set ; :: according to FUNCOP_1:def_6,YELLOW14:def_2 ::_thesis: ( not x in dom the mapping of N or the mapping of N . x is set )
assume  x in dom the mapping of N ; ::_thesis: the mapping of N . x is set
then  the mapping of N . x in rng the mapping of N by FUNCT_1:def_3;
hence  the mapping of N . x is set ; ::_thesis: verum
end;
end;

registration
let R be constituted-Functions 1-sorted ;
cluster strict Function-yielding for NetStr over R;
existence
 ex b1 being NetStr over R st
( b1 is strict & b1 is Function-yielding )
proof
take A = NetStr(# the carrier of R,(id the carrier of R),(id the carrier of R) #); ::_thesis: ( A is strict & A is Function-yielding )
thus  A is strict ; ::_thesis: A is Function-yielding
let x be set ; :: according to FUNCOP_1:def_6,YELLOW14:def_2 ::_thesis: ( not x in dom the mapping of A or the mapping of A . x is set )
assume  x in dom the mapping of A ; ::_thesis: the mapping of A . x is set
hence  the mapping of A . x is set by FUNCT_1:18; ::_thesis: verum
end;
end;

registration
let R be non empty constituted-Functions 1-sorted ;
cluster non empty strict Function-yielding for NetStr over R;
existence
 ex b1 being NetStr over R st
( b1 is strict & not b1 is empty & b1 is Function-yielding )
proof
take A = NetStr(# the carrier of R,(id the carrier of R),(id the carrier of R) #); ::_thesis: ( A is strict & not A is empty & A is Function-yielding )
thus  ( A is strict & not A is empty ) ; ::_thesis: A is Function-yielding
let x be set ; :: according to FUNCOP_1:def_6,YELLOW14:def_2 ::_thesis: ( not x in dom the mapping of A or the mapping of A . x is set )
assume  x in dom the mapping of A ; ::_thesis: the mapping of A . x is set
hence  the mapping of A . x is set by FUNCT_1:18; ::_thesis: verum
end;
end;

registration
let R be constituted-Functions 1-sorted ;
let N be Function-yielding NetStr over R;
cluster the mapping of N ->  Function-yielding ;
coherence
 the mapping of N is Function-yielding by Def2;
end;

registration
let R be non empty constituted-Functions 1-sorted ;
cluster non empty transitive strict directed Function-yielding for NetStr over R;
existence
 ex b1 being net of R st
( b1 is strict & b1 is Function-yielding )
proof
set p = the Element of R;
set N = the net of R;
take  ConstantNet ( the net of R, the Element of R) ; ::_thesis: ( ConstantNet ( the net of R, the Element of R) is strict & ConstantNet ( the net of R, the Element of R) is Function-yielding )
thus  ( ConstantNet ( the net of R, the Element of R) is strict & ConstantNet ( the net of R, the Element of R) is Function-yielding ) ; ::_thesis: verum
end;
end;

registration
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
cluster rng the mapping of N ->  non empty ;
coherence
 not rng the mapping of N is empty ;
end;

registration
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
cluster rng (netmap (N,S)) ->  non empty ;
coherence
 not rng (netmap (N,S)) is empty ;
end;

theorem :: YELLOW14:7
for A, B, C being non empty RelStr
for f being Function of B,C
for g, h being Function of A,B st g <= h & f is monotone holds
f * g <= f * h
proof
let A, B, C be non empty RelStr ; ::_thesis: for f being Function of B,C
for g, h being Function of A,B st g <= h & f is monotone holds
f * g <= f * h
let f be Function of B,C; ::_thesis: for g, h being Function of A,B st g <= h & f is monotone holds
f * g <= f * h
let g, h be Function of A,B; ::_thesis: ( g <= h & f is monotone implies f * g <= f * h )
assume that
A1: g <= h and
A2: for x, y being Element of B st x <= y holds
f . x <= f . y ; :: according to WAYBEL_1:def_2 ::_thesis: f * g <= f * h
 for x being Element of A holds (f * g) . x <= (f * h) . x
proof
let x be Element of A; ::_thesis: (f * g) . x <= (f * h) . x
A3: ( (f * g) . x = f . (g . x) & (f * h) . x = f . (h . x) ) by FUNCT_2:15;
 g . x <= h . x by A1, YELLOW_2:9;
hence  (f * g) . x <= (f * h) . x by A2, A3; ::_thesis: verum
end;
hence  f * g <= f * h by YELLOW_2:9; ::_thesis: verum
end;

theorem :: YELLOW14:8
for S being non empty TopSpace
for T being non empty TopSpace-like TopRelStr
for f, g being Function of S,T
for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
proof
let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like TopRelStr
for f, g being Function of S,T
for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
let T be non empty TopSpace-like TopRelStr ; ::_thesis: for f, g being Function of S,T
for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
let f, g be Function of S,T; ::_thesis: for x, y being Element of (ContMaps (S,T)) st x = f & y = g holds
( x <= y iff f <= g )
let x, y be Element of (ContMaps (S,T)); ::_thesis: ( x = f & y = g implies ( x <= y iff f <= g ) )
assume A1: ( x = f & y = g ) ; ::_thesis: ( x <= y iff f <= g )
A2: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by WAYBEL24:def_3;
then reconsider x1 = x, y1 = y as Element of (T |^ the carrier of S) by YELLOW_0:58;
hereby  ::_thesis: ( f <= g implies x <= y )
assume  x <= y ; ::_thesis: f <= g
then  x1 <= y1 by A2, YELLOW_0:59;
hence  f <= g by A1, WAYBEL10:11; ::_thesis: verum
end;
assume  f <= g ; ::_thesis: x <= y
then  x1 <= y1 by A1, WAYBEL10:11;
hence  x <= y by A2, YELLOW_0:60; ::_thesis: verum
end;

definition
let I be non empty set ;
let R be non empty RelStr ;
let f be Element of (R |^ I);
let i be Element of I;
:: original: .
redefine funcf . i ->  Element of R;
coherence
 f . i is Element of R
proof
reconsider g = f as Element of (product (I --> R)) by YELLOW_1:def_5;
 g . i is Element of ((I --> R) . i) ;
hence  f . i is Element of R by FUNCOP_1:7; ::_thesis: verum
end;
end;

begin

theorem Th9: :: YELLOW14:9
for S, T being RelStr
for f being Function of S,T st f is isomorphic holds
f is onto
proof
let S, T be RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds
f is onto
let f be Function of S,T; ::_thesis: ( f is isomorphic implies f is onto )
assume A1: f is isomorphic ; ::_thesis: f is onto
percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
suppose ( not S is empty & not T is empty ) ; ::_thesis: f is onto
hence  rng f = the carrier of T by A1, WAYBEL_0:66; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
suppose ( S is empty or T is empty ) ; ::_thesis: f is onto
then  T is empty by A1, WAYBEL_0:def_38;
then  the carrier of T = {} ;
hence  rng f = the carrier of T ; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;
end;

registration
let S, T be RelStr ;
cluster Function-like quasi_total isomorphic  ->  onto for Element of K6(K7( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is isomorphic holds
b1 is onto by Th9;
end;

theorem Th10: :: YELLOW14:10
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
f /" is isomorphic
proof
let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T st f is isomorphic holds
f /" is isomorphic
let f be Function of S,T; ::_thesis: ( f is isomorphic implies f /" is isomorphic )
assume A1: f is isomorphic ; ::_thesis: f /" is isomorphic
then  ( ex g being Function of T,S st
( g = f " & g is monotone ) & rng f = the carrier of T ) by WAYBEL_0:66, WAYBEL_0:def_38;
hence  f /" is isomorphic by A1, TOPS_2:def_4, WAYBEL_0:68; ::_thesis: verum
end;

theorem :: YELLOW14:11
for S, T being non empty RelStr st S,T are_isomorphic & S is with_infima holds
T is with_infima
proof
let S, T be non empty RelStr ; ::_thesis: ( S,T are_isomorphic & S is with_infima implies T is with_infima )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is with_infima or T is with_infima )
assume A2: for a, b being Element of S ex c being Element of S st
( c <= a & c <= b & ( for c9 being Element of S st c9 <= a & c9 <= b holds
c9 <= c ) ) ; :: according to LATTICE3:def_11 ::_thesis: T is with_infima
let x, y be Element of T; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of T st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of T holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
consider c being Element of S such that
A3: ( c <= (f /") . x & c <= (f /") . y ) and
A4: for c9 being Element of S st c9 <= (f /") . x & c9 <= (f /") . y holds
c9 <= c by A2;
take  f . c ; ::_thesis: ( f . c <= x & f . c <= y & ( for b1 being Element of the carrier of T holds
( not b1 <= x or not b1 <= y or b1 <= f . c ) ) )
A5: ex g being Function of T,S st
( g = f " & g is monotone ) by A1, WAYBEL_0:def_38;
A6: rng f = the carrier of T by A1, WAYBEL_0:66;
A7: f /" = f " by A1, TOPS_2:def_4;
 ( f . c <= f . ((f /") . x) & f . c <= f . ((f /") . y) ) by A1, A3, WAYBEL_0:66;
hence  ( f . c <= x & f . c <= y ) by A1, A6, A7, FUNCT_1:35; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 <= x or not b1 <= y or b1 <= f . c )
let z9 be Element of T; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= f . c )
assume  ( z9 <= x & z9 <= y ) ; ::_thesis: z9 <= f . c
then  ( (f /") . z9 <= (f /") . x & (f /") . z9 <= (f /") . y ) by A7, A5, WAYBEL_1:def_2;
then  (f /") . z9 <= c by A4;
then  f . ((f /") . z9) <= f . c by A1, WAYBEL_0:66;
hence  z9 <= f . c by A1, A6, A7, FUNCT_1:35; ::_thesis: verum
end;

theorem :: YELLOW14:12
for S, T being non empty RelStr st S,T are_isomorphic & S is with_suprema holds
T is with_suprema
proof
let S, T be non empty RelStr ; ::_thesis: ( S,T are_isomorphic & S is with_suprema implies T is with_suprema )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is with_suprema or T is with_suprema )
assume A2: for a, b being Element of S ex c being Element of S st
( a <= c & b <= c & ( for c9 being Element of S st a <= c9 & b <= c9 holds
c <= c9 ) ) ; :: according to LATTICE3:def_10 ::_thesis: T is with_suprema
let x, y be Element of T; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of T st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of T holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
consider c being Element of S such that
A3: ( (f /") . x <= c & (f /") . y <= c ) and
A4: for c9 being Element of S st (f /") . x <= c9 & (f /") . y <= c9 holds
c <= c9 by A2;
take  f . c ; ::_thesis: ( x <= f . c & y <= f . c & ( for b1 being Element of the carrier of T holds
( not x <= b1 or not y <= b1 or f . c <= b1 ) ) )
A5: ex g being Function of T,S st
( g = f " & g is monotone ) by A1, WAYBEL_0:def_38;
A6: rng f = the carrier of T by A1, WAYBEL_0:66;
A7: f /" = f " by A1, TOPS_2:def_4;
 ( f . ((f /") . x) <= f . c & f . ((f /") . y) <= f . c ) by A1, A3, WAYBEL_0:66;
hence  ( x <= f . c & y <= f . c ) by A1, A6, A7, FUNCT_1:35; ::_thesis: for b1 being Element of the carrier of T holds
( not x <= b1 or not y <= b1 or f . c <= b1 )
let z9 be Element of T; ::_thesis: ( not x <= z9 or not y <= z9 or f . c <= z9 )
assume  ( x <= z9 & y <= z9 ) ; ::_thesis: f . c <= z9
then  ( (f /") . x <= (f /") . z9 & (f /") . y <= (f /") . z9 ) by A7, A5, WAYBEL_1:def_2;
then  c <= (f /") . z9 by A4;
then  f . c <= f . ((f /") . z9) by A1, WAYBEL_0:66;
hence  f . c <= z9 by A1, A6, A7, FUNCT_1:35; ::_thesis: verum
end;

theorem Th13: :: YELLOW14:13
for L being RelStr st L is empty holds
L is bounded
proof
let L be RelStr ; ::_thesis: ( L is empty implies L is bounded )
assume A1: L is empty ; ::_thesis: L is bounded
set x = the Element of L;
thus  L is lower-bounded :: according to YELLOW_0:def_6 ::_thesis: L is upper-bounded
proof
take  the Element of L ; :: according to YELLOW_0:def_4 ::_thesis: the Element of L is_<=_than the carrier of L
let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in the carrier of L or the Element of L <= a )
assume  a in the carrier of L ; ::_thesis: the Element of L <= a
hence  the Element of L <= a by A1; ::_thesis: verum
end;
take  the Element of L ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of L is_<=_than the Element of L
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in the carrier of L or a <= the Element of L )
assume  a in the carrier of L ; ::_thesis: a <= the Element of L
hence  a <= the Element of L by A1; ::_thesis: verum
end;

registration
cluster empty  ->  bounded for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
b1 is bounded by Th13;
end;

theorem :: YELLOW14:14
for S, T being RelStr st S,T are_isomorphic & S is lower-bounded holds
T is lower-bounded
proof
let S, T be RelStr ; ::_thesis: ( S,T are_isomorphic & S is lower-bounded implies T is lower-bounded )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is lower-bounded or T is lower-bounded )
percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
suppose ( not S is empty & not T is empty ) ; ::_thesis: ( not S is lower-bounded or T is lower-bounded )
then reconsider s = S, t = T as non empty RelStr ;
given X being Element of S such that A2: X is_<=_than the carrier of S ; :: according to YELLOW_0:def_4 ::_thesis: T is lower-bounded
reconsider x = X as Element of s ;
reconsider g = f as Function of s,t ;
reconsider y = g . x as Element of T ;
take  y ; :: according to YELLOW_0:def_4 ::_thesis: y is_<=_than the carrier of T
 y is_<=_than g .: ([#] S) by A1, A2, YELLOW_2:13;
then  y is_<=_than rng g by RELSET_1:22;
hence  y is_<=_than the carrier of T by A1, WAYBEL_0:66; ::_thesis: verum
end;
suppose ( S is empty or T is empty ) ; ::_thesis: ( not S is lower-bounded or T is lower-bounded )
then  T is empty by A1, WAYBEL_0:def_38;
then reconsider T = T as bounded RelStr ;
 T is lower-bounded ;
hence  ( not S is lower-bounded or T is lower-bounded ) ; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW14:15
for S, T being RelStr st S,T are_isomorphic & S is upper-bounded holds
T is upper-bounded
proof
let S, T be RelStr ; ::_thesis: ( S,T are_isomorphic & S is upper-bounded implies T is upper-bounded )
given f being Function of S,T such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not S is upper-bounded or T is upper-bounded )
percases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
suppose ( not S is empty & not T is empty ) ; ::_thesis: ( not S is upper-bounded or T is upper-bounded )
then reconsider s = S, t = T as non empty RelStr ;
given X being Element of S such that A2: X is_>=_than the carrier of S ; :: according to YELLOW_0:def_5 ::_thesis: T is upper-bounded
reconsider x = X as Element of s ;
reconsider g = f as Function of s,t ;
reconsider y = g . x as Element of T ;
take  y ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of T is_<=_than y
 y is_>=_than g .: ([#] S) by A1, A2, YELLOW_2:14;
then  y is_>=_than rng g by RELSET_1:22;
hence  the carrier of T is_<=_than y by A1, WAYBEL_0:66; ::_thesis: verum
end;
suppose ( S is empty or T is empty ) ; ::_thesis: ( not S is upper-bounded or T is upper-bounded )
then  T is empty by A1, WAYBEL_0:def_38;
then reconsider T = T as bounded RelStr ;
 T is lower-bounded ;
hence  ( not S is upper-bounded or T is upper-bounded ) ; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW14:16
for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
proof
let S, T be non empty RelStr ; ::_thesis: for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
let A be Subset of S; ::_thesis: for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
let f be Function of S,T; ::_thesis: ( f is isomorphic & ex_sup_of A,S implies ex_sup_of f .: A,T )
assume A1: f is isomorphic ; ::_thesis: ( not ex_sup_of A,S or ex_sup_of f .: A,T )
A2: f " (f .: A) c= A by A1, FUNCT_1:82;
A3: rng f = [#] T by A1, WAYBEL_0:66;
A4: f /" = f " by A1, TOPS_2:def_4;
given a being Element of S such that A5: A is_<=_than a and
A6: for b being Element of S st A is_<=_than b holds
b >= a and
A7: for c being Element of S st A is_<=_than c & ( for b being Element of S st A is_<=_than b holds
b >= c ) holds
c = a ; :: according to YELLOW_0:def_7 ::_thesis: ex_sup_of f .: A,T
take  f . a ; :: according to YELLOW_0:def_7 ::_thesis: ( f .: A is_<=_than f . a & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) )
thus  f .: A is_<=_than f . a by A1, A5, WAYBEL13:19; ::_thesis: ( ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) )
A8: f /" is isomorphic by A1, Th10;
A9: dom f = the carrier of S by FUNCT_2:def_1;
then  A c= f " (f .: A) by FUNCT_1:76;
then A10: f " (f .: A) = A by A2, XBOOLE_0:def_10;
hereby  ::_thesis: for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a )
let b be Element of T; ::_thesis: ( f .: A is_<=_than b implies b >= f . a )
assume  f .: A is_<=_than b ; ::_thesis: b >= f . a
then  (f /") .: (f .: A) is_<=_than (f /") . b by A8, WAYBEL13:19;
then  f " (f .: A) is_<=_than (f /") . b by A1, A3, TOPS_2:55;
then  (f /") . b >= a by A6, A10;
then  f . ((f /") . b) >= f . a by A1, WAYBEL_0:66;
hence  b >= f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum
end;
let c be Element of T; ::_thesis: ( not f .: A is_<=_than c or ex b1 being Element of the carrier of T st
( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a )
assume A11: f .: A is_<=_than c ; ::_thesis: ( ex b1 being Element of the carrier of T st
( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a )
assume A12: for b being Element of T st f .: A is_<=_than b holds
b >= c ; ::_thesis: c = f . a
A13: for b being Element of S st A is_<=_than b holds
b >= (f /") . c
proof
let b be Element of S; ::_thesis: ( A is_<=_than b implies b >= (f /") . c )
assume  A is_<=_than b ; ::_thesis: b >= (f /") . c
then  f .: A is_<=_than f . b by A1, WAYBEL13:19;
then  f . b >= c by A12;
then  (f /") . (f . b) >= (f /") . c by A8, WAYBEL_0:66;
hence  b >= (f /") . c by A1, A4, A9, FUNCT_1:34; ::_thesis: verum
end;
 (f /") .: (f .: A) is_<=_than (f /") . c by A8, A11, WAYBEL13:19;
then  A is_<=_than (f /") . c by A1, A3, A10, TOPS_2:55;
then  (f /") . c = a by A7, A13;
hence  c = f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum
end;

theorem :: YELLOW14:17
for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds
ex_inf_of f .: A,T
proof
let S, T be non empty RelStr ; ::_thesis: for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds
ex_inf_of f .: A,T
let A be Subset of S; ::_thesis: for f being Function of S,T st f is isomorphic & ex_inf_of A,S holds
ex_inf_of f .: A,T
let f be Function of S,T; ::_thesis: ( f is isomorphic & ex_inf_of A,S implies ex_inf_of f .: A,T )
assume A1: f is isomorphic ; ::_thesis: ( not ex_inf_of A,S or ex_inf_of f .: A,T )
A2: f " (f .: A) c= A by A1, FUNCT_1:82;
A3: rng f = [#] T by A1, WAYBEL_0:66;
A4: f /" = f " by A1, TOPS_2:def_4;
given a being Element of S such that A5: A is_>=_than a and
A6: for b being Element of S st A is_>=_than b holds
b <= a and
A7: for c being Element of S st A is_>=_than c & ( for b being Element of S st A is_>=_than b holds
b <= c ) holds
c = a ; :: according to YELLOW_0:def_8 ::_thesis: ex_inf_of f .: A,T
take  f . a ; :: according to YELLOW_0:def_8 ::_thesis: ( f . a is_<=_than f .: A & ( for b1 being Element of the carrier of T holds
( not b1 is_<=_than f .: A or b1 <= f . a ) ) & ( for b1 being Element of the carrier of T holds
( not b1 is_<=_than f .: A or ex b2 being Element of the carrier of T st
( b2 is_<=_than f .: A & not b2 <= b1 ) or b1 = f . a ) ) )
thus  f .: A is_>=_than f . a by A1, A5, WAYBEL13:18; ::_thesis: ( ( for b1 being Element of the carrier of T holds
( not b1 is_<=_than f .: A or b1 <= f . a ) ) & ( for b1 being Element of the carrier of T holds
( not b1 is_<=_than f .: A or ex b2 being Element of the carrier of T st
( b2 is_<=_than f .: A & not b2 <= b1 ) or b1 = f . a ) ) )
A8: f /" is isomorphic by A1, Th10;
A9: dom f = the carrier of S by FUNCT_2:def_1;
then  A c= f " (f .: A) by FUNCT_1:76;
then A10: f " (f .: A) = A by A2, XBOOLE_0:def_10;
hereby  ::_thesis: for b1 being Element of the carrier of T holds
( not b1 is_<=_than f .: A or ex b2 being Element of the carrier of T st
( b2 is_<=_than f .: A & not b2 <= b1 ) or b1 = f . a )
let b be Element of T; ::_thesis: ( f .: A is_>=_than b implies b <= f . a )
assume  f .: A is_>=_than b ; ::_thesis: b <= f . a
then  (f /") .: (f .: A) is_>=_than (f /") . b by A8, WAYBEL13:18;
then  f " (f .: A) is_>=_than (f /") . b by A1, A3, TOPS_2:55;
then  (f /") . b <= a by A6, A10;
then  f . ((f /") . b) <= f . a by A1, WAYBEL_0:66;
hence  b <= f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum
end;
let c be Element of T; ::_thesis: ( not c is_<=_than f .: A or ex b1 being Element of the carrier of T st
( b1 is_<=_than f .: A & not b1 <= c ) or c = f . a )
assume A11: f .: A is_>=_than c ; ::_thesis: ( ex b1 being Element of the carrier of T st
( b1 is_<=_than f .: A & not b1 <= c ) or c = f . a )
assume A12: for b being Element of T st f .: A is_>=_than b holds
b <= c ; ::_thesis: c = f . a
A13: for b being Element of S st A is_>=_than b holds
b <= (f /") . c
proof
let b be Element of S; ::_thesis: ( A is_>=_than b implies b <= (f /") . c )
assume  A is_>=_than b ; ::_thesis: b <= (f /") . c
then  f .: A is_>=_than f . b by A1, WAYBEL13:18;
then  f . b <= c by A12;
then  (f /") . (f . b) <= (f /") . c by A8, WAYBEL_0:66;
hence  b <= (f /") . c by A1, A4, A9, FUNCT_1:34; ::_thesis: verum
end;
 (f /") .: (f .: A) is_>=_than (f /") . c by A8, A11, WAYBEL13:18;
then  A is_>=_than (f /") . c by A1, A3, A10, TOPS_2:55;
then  (f /") . c = a by A7, A13;
hence  c = f . a by A1, A3, A4, FUNCT_1:35; ::_thesis: verum
end;

begin

theorem :: YELLOW14:18
for S, T being TopStruct st ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) holds
( S is empty iff T is empty )
proof
let S, T be TopStruct ; ::_thesis: ( ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) implies ( S is empty iff T is empty ) )
assume A1: ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) ; ::_thesis: ( S is empty iff T is empty )
percases ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ) by A1;
suppose S,T are_homeomorphic ; ::_thesis: ( S is empty iff T is empty )
then consider f being Function of S,T such that
A2: f is being_homeomorphism by T_0TOPSP:def_1;
 ( rng f = [#] T & dom f = [#] S ) by A2, TOPS_2:def_5;
hence  ( S is empty iff T is empty ) ; ::_thesis: verum
end;
suppose ex f being Function of S,T st
( dom f = [#] S & rng f = [#] T ) ; ::_thesis: ( S is empty iff T is empty )
hence  ( S is empty iff T is empty ) ; ::_thesis: verum
end;
end;
end;

theorem :: YELLOW14:19
for T being non empty TopSpace holds T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic
proof
let T be non empty TopSpace; ::_thesis: T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic
reconsider f = id T as Function of T,TopStruct(# the carrier of T, the topology of T #) ;
take  f ; :: according to T_0TOPSP:def_1 ::_thesis: f is being_homeomorphism
thus  dom f = [#] T by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] TopStruct(# the carrier of T, the topology of T #) & f is one-to-one & f is continuous & f /" is continuous )
thus  rng f = [#] T by TOPS_2:def_5
.= [#] TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: ( f is one-to-one & f is continuous & f /" is continuous )
thus  f is V14() ; ::_thesis: ( f is continuous & f /" is continuous )
thus  f is continuous by YELLOW12:36; ::_thesis: f /" is continuous
thus  f /" is continuous by YELLOW12:36; ::_thesis: verum
end;

registration
let T be non empty reflexive Scott TopRelStr ;
cluster open  ->  upper inaccessible for Element of K6( the carrier of T);
coherence
 for b1 being Subset of T st b1 is open holds
( b1 is inaccessible & b1 is upper ) by WAYBEL11:def_4;
cluster upper inaccessible  ->  open for Element of K6( the carrier of T);
coherence
 for b1 being Subset of T st b1 is inaccessible & b1 is upper holds
b1 is open by WAYBEL11:def_4;
end;

theorem :: YELLOW14:20
for T being TopStruct
for x, y being Point of T
for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
x in Cl Y
proof
let T be TopStruct ; ::_thesis: for x, y being Point of T
for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
x in Cl Y
let x, y be Point of T; ::_thesis: for X, Y being Subset of T st X = {x} & Cl X c= Cl Y holds
x in Cl Y
let X, Y be Subset of T; ::_thesis: ( X = {x} & Cl X c= Cl Y implies x in Cl Y )
assume that
A1: X = {x} and
A2: Cl X c= Cl Y ; ::_thesis: x in Cl Y
 X c= Cl X by PRE_TOPC:18;
then A3: X c= Cl Y by A2, XBOOLE_1:1;
 x in X by A1, TARSKI:def_1;
hence  x in Cl Y by A3; ::_thesis: verum
end;

theorem :: YELLOW14:21
for T being TopStruct
for x, y being Point of T
for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V
proof
let T be TopStruct ; ::_thesis: for x, y being Point of T
for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V
let x, y be Point of T; ::_thesis: for Y, V being Subset of T st Y = {y} & x in Cl Y & V is open & x in V holds
y in V
let Y, V be Subset of T; ::_thesis: ( Y = {y} & x in Cl Y & V is open & x in V implies y in V )
assume A1: Y = {y} ; ::_thesis: ( not x in Cl Y or not V is open or not x in V or y in V )
assume  ( x in Cl Y & V is open & x in V ) ; ::_thesis: y in V
then  Y meets V by PRE_TOPC:def_7;
hence  y in V by A1, ZFMISC_1:50; ::_thesis: verum
end;

theorem :: YELLOW14:22
for T being TopStruct
for x, y being Point of T
for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) holds
Cl X c= Cl Y
proof
let T be TopStruct ; ::_thesis: for x, y being Point of T
for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) holds
Cl X c= Cl Y
let x, y be Point of T; ::_thesis: for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) holds
Cl X c= Cl Y
let X, Y be Subset of T; ::_thesis: ( X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) implies Cl X c= Cl Y )
assume that
A1: X = {x} and
A2: ( Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) ) ; ::_thesis: Cl X c= Cl Y
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Cl X or z in Cl Y )
assume A3: z in Cl X ; ::_thesis: z in Cl Y
 for V being Subset of T st V is open & z in V holds
Y meets V
proof
let V be Subset of T; ::_thesis: ( V is open & z in V implies Y meets V )
assume that
A4: V is open and
A5: z in V ; ::_thesis: Y meets V
 X meets V by A3, A4, A5, PRE_TOPC:def_7;
then  x in V by A1, ZFMISC_1:50;
hence  Y meets V by A2, A4, ZFMISC_1:48; ::_thesis: verum
end;
hence  z in Cl Y by A3, PRE_TOPC:def_7; ::_thesis: verum
end;

theorem Th23: :: YELLOW14:23
for S, T being non empty TopSpace
for A being irreducible Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is irreducible
proof
let S, T be non empty TopSpace; ::_thesis: for A being irreducible Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is irreducible
let A be irreducible Subset of S; ::_thesis: for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is irreducible
let B be Subset of T; ::_thesis: ( A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) implies B is irreducible )
assume that
A1: A = B and
A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: B is irreducible
 ( not A is empty & A is closed ) by YELLOW_8:def_3;
hence  ( not B is empty & B is closed ) by A1, A2, TOPS_3:79; :: according to YELLOW_8:def_3 ::_thesis: for b1, b2 being Element of K6( the carrier of T) holds
( not b1 is closed or not b2 is closed or not B = K20(K6( the carrier of T),b1,b2) or b1 = B or b2 = B )
let B1, B2 be Subset of T; ::_thesis: ( not B1 is closed or not B2 is closed or not B = K20(K6( the carrier of T),B1,B2) or B1 = B or B2 = B )
assume that
A3: ( B1 is closed & B2 is closed ) and
A4: B = B1 \/ B2 ; ::_thesis: ( B1 = B or B2 = B )
reconsider A1 = B1, A2 = B2 as Subset of S by A2;
 ( A1 is closed & A2 is closed ) by A2, A3, TOPS_3:79;
hence  ( B1 = B or B2 = B ) by A1, A4, YELLOW_8:def_3; ::_thesis: verum
end;

theorem Th24: :: YELLOW14:24
for S, T being non empty TopSpace
for a being Point of S
for b being Point of T
for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
proof
let S, T be non empty TopSpace; ::_thesis: for a being Point of S
for b being Point of T
for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let a be Point of S; ::_thesis: for b being Point of T
for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let b be Point of T; ::_thesis: for A being Subset of S
for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let A be Subset of S; ::_thesis: for B being Subset of T st a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
let B be Subset of T; ::_thesis: ( a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A implies b is_dense_point_of B )
assume  ( a = b & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a in A & A c= Cl {a} ) ; :: according to YELLOW_8:def_4 ::_thesis: b is_dense_point_of B
hence  ( b in B & B c= Cl {b} ) by TOPS_3:80; :: according to YELLOW_8:def_4 ::_thesis: verum
end;

theorem Th25: :: YELLOW14:25
for S, T being TopStruct
for A being Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds
B is compact
proof
let S, T be TopStruct ; ::_thesis: for A being Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds
B is compact
let A be Subset of S; ::_thesis: for B being Subset of T st A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact holds
B is compact
let B be Subset of T; ::_thesis: ( A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & A is compact implies B is compact )
assume that
A1: A = B and
A2: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A3: for F being Subset-Family of S st F is Cover of A & F is open holds
ex G being Subset-Family of S st
( G c= F & G is Cover of A & G is finite ) ; :: according to COMPTS_1:def_4 ::_thesis: B is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( not F is Cover of B or not F is open or ex b1 being Element of K6(K6( the carrier of T)) st
( b1 c= F & b1 is Cover of B & b1 is finite ) )
assume A4: ( F is Cover of B & F is open ) ; ::_thesis: ex b1 being Element of K6(K6( the carrier of T)) st
( b1 c= F & b1 is Cover of B & b1 is finite )
reconsider K = F as Subset-Family of S by A2;
consider L being Subset-Family of S such that
A5: ( L c= K & L is Cover of A & L is finite ) by A1, A2, A3, A4, WAYBEL_9:19;
reconsider G = L as Subset-Family of T by A2;
take  G ; ::_thesis: ( G c= F & G is Cover of B & G is finite )
thus  ( G c= F & G is Cover of B & G is finite ) by A1, A5; ::_thesis: verum
end;

theorem :: YELLOW14:26
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is sober holds
T is sober
proof
let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is sober implies T is sober )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: for A being irreducible Subset of S ex a being Point of S st
( a is_dense_point_of A & ( for b being Point of S st b is_dense_point_of A holds
a = b ) ) ; :: according to YELLOW_8:def_5 ::_thesis: T is sober
let B be irreducible Subset of T; :: according to YELLOW_8:def_5 ::_thesis: ex b1 being Element of the carrier of T st
( b1 is_dense_point_of B & ( for b2 being Element of the carrier of T holds
( not b2 is_dense_point_of B or b1 = b2 ) ) )
reconsider A = B as irreducible Subset of S by A1, Th23;
consider a being Point of S such that
A3: a is_dense_point_of A and
A4: for b being Point of S st b is_dense_point_of A holds
a = b by A2;
reconsider p = a as Point of T by A1;
take  p ; ::_thesis: ( p is_dense_point_of B & ( for b1 being Element of the carrier of T holds
( not b1 is_dense_point_of B or p = b1 ) ) )
thus  p is_dense_point_of B by A1, A3, Th24; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 is_dense_point_of B or p = b1 )
let q be Point of T; ::_thesis: ( not q is_dense_point_of B or p = q )
reconsider b = q as Point of S by A1;
assume  q is_dense_point_of B ; ::_thesis: p = q
then  b is_dense_point_of A by A1, Th24;
hence  p = q by A4; ::_thesis: verum
end;

theorem :: YELLOW14:27
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally-compact holds
T is locally-compact
proof
let S, T be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is locally-compact implies T is locally-compact )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: for x being Point of S
for X being Subset of S st x in X & X is open holds
ex Y being Subset of S st
( x in Int Y & Y c= X & Y is compact ) ; :: according to WAYBEL_3:def_9 ::_thesis: T is locally-compact
let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of K6( the carrier of T) holds
( not x in b1 or not b1 is open or ex b2 being Element of K6( the carrier of T) st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of T; ::_thesis: ( not x in X or not X is open or ex b1 being Element of K6( the carrier of T) st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume A3: ( x in X & X is open ) ; ::_thesis: ex b1 being Element of K6( the carrier of T) st
( x in Int b1 & b1 c= X & b1 is compact )
reconsider A = X as Subset of S by A1;
consider B being Subset of S such that
A4: ( x in Int B & B c= A & B is compact ) by A1, A2, A3, TOPS_3:76;
reconsider Y = B as Subset of T by A1;
take  Y ; ::_thesis: ( x in Int Y & Y c= X & Y is compact )
thus  ( x in Int Y & Y c= X & Y is compact ) by A1, A4, Th25, TOPS_3:77; ::_thesis: verum
end;

theorem :: YELLOW14:28
for S, T being TopStruct st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is compact holds
T is compact
proof
let S, T be TopStruct ; ::_thesis: ( TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & S is compact implies T is compact )
assume that
A1: TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) and
A2: for F being Subset-Family of S st F is Cover of S & F is open holds
ex G being Subset-Family of S st
( G c= F & G is Cover of S & G is finite ) ; :: according to COMPTS_1:def_1 ::_thesis: T is compact
let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( not F is Cover of the carrier of T or not F is open or ex b1 being Element of K6(K6( the carrier of T)) st
( b1 c= F & b1 is Cover of the carrier of T & b1 is finite ) )
assume A3: ( F is Cover of T & F is open ) ; ::_thesis: ex b1 being Element of K6(K6( the carrier of T)) st
( b1 c= F & b1 is Cover of the carrier of T & b1 is finite )
reconsider K = F as Subset-Family of S by A1;
consider L being Subset-Family of S such that
A4: ( L c= K & L is Cover of S & L is finite ) by A1, A2, A3, WAYBEL_9:19;
reconsider G = L as Subset-Family of T by A1;
take  G ; ::_thesis: ( G c= F & G is Cover of the carrier of T & G is finite )
thus  ( G c= F & G is Cover of the carrier of T & G is finite ) by A1, A4; ::_thesis: verum
end;

definition
let I be non empty set ;
let T be non empty TopSpace;
let x be Point of (product (I --> T));
let i be Element of I;
:: original: .
redefine funcx . i ->  Element of T;
coherence
 x . i is Element of T
proof
 x . i is Point of T by FUNCOP_1:7;
hence  x . i is Element of T ; ::_thesis: verum
end;
end;

theorem Th29: :: YELLOW14:29
for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
proof
let M be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M
for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let x, y be Point of (product J); ::_thesis: ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
hereby  ::_thesis: ( ( for i being Element of M holds x . i in Cl {(y . i)} ) implies x in Cl {y} )
assume A1: x in Cl {y} ; ::_thesis: for i being Element of M holds x . i in Cl {(y . i)}
let i be Element of M; ::_thesis: x . i in Cl {(y . i)}
 x in the carrier of (product J) ;
then  x in product (Carrier J) by WAYBEL18:def_3;
then consider f being Function such that
A2: x = f and
A3: dom f = dom (Carrier J) and
A4: for z being set st z in dom (Carrier J) holds
f . z in (Carrier J) . z by CARD_3:def_5;
A5: i in M ;
 for G being Subset of (J . i) st G is open & x . i in G holds
{(y . i)} meets G
proof
let G be Subset of (J . i); ::_thesis: ( G is open & x . i in G implies {(y . i)} meets G )
assume that
A6: G is open and
A7: x . i in G ; ::_thesis: {(y . i)} meets G
reconsider G9 = G as Subset of (J . i) ;
 ( [#] (J . i) <> {} & proj (J,i) is continuous ) by WAYBEL18:5;
then A8: (proj (J,i)) " G9 is open by A6, TOPS_2:43;
A9: for z being set st z in dom ((Carrier J) +* (i,G)) holds
f . z in ((Carrier J) +* (i,G)) . z
proof
let z be set ; ::_thesis: ( z in dom ((Carrier J) +* (i,G)) implies f . z in ((Carrier J) +* (i,G)) . z )
assume  z in dom ((Carrier J) +* (i,G)) ; ::_thesis: f . z in ((Carrier J) +* (i,G)) . z
then A10: z in dom (Carrier J) by FUNCT_7:30;
percases ( z = i or z <> i ) ;
suppose z = i ; ::_thesis: f . z in ((Carrier J) +* (i,G)) . z
hence  f . z in ((Carrier J) +* (i,G)) . z by A2, A7, A10, FUNCT_7:31; ::_thesis: verum
end;
suppose z <> i ; ::_thesis: f . z in ((Carrier J) +* (i,G)) . z
then  ((Carrier J) +* (i,G)) . z = (Carrier J) . z by FUNCT_7:32;
hence  f . z in ((Carrier J) +* (i,G)) . z by A4, A10; ::_thesis: verum
end;
end;
end;
A11: product ((Carrier J) +* (i,G9)) = (proj (J,i)) " G9 by WAYBEL18:4;
 dom f = dom ((Carrier J) +* (i,G)) by A3, FUNCT_7:30;
then  x in product ((Carrier J) +* (i,G)) by A2, A9, CARD_3:def_5;
then  {y} meets (proj (J,i)) " G9 by A1, A8, A11, PRE_TOPC:def_7;
then  y in product ((Carrier J) +* (i,G)) by A11, ZFMISC_1:50;
then consider g being Function such that
A12: y = g and
 dom g = dom ((Carrier J) +* (i,G)) and
A13: for z being set st z in dom ((Carrier J) +* (i,G)) holds
g . z in ((Carrier J) +* (i,G)) . z by CARD_3:def_5;
A14: i in dom (Carrier J) by A5, PARTFUN1:def_2;
then  i in dom ((Carrier J) +* (i,G)) by FUNCT_7:30;
then  g . i in ((Carrier J) +* (i,G)) . i by A13;
then  g . i in G by A14, FUNCT_7:31;
hence  {(y . i)} meets G by A12, ZFMISC_1:48; ::_thesis: verum
end;
hence  x . i in Cl {(y . i)} by PRE_TOPC:def_7; ::_thesis: verum
end;
reconsider K = product_prebasis J as prebasis of (product J) by WAYBEL18:def_3;
assume A15: for i being Element of M holds x . i in Cl {(y . i)} ; ::_thesis: x in Cl {y}
 for Z being finite Subset-Family of (product J) st Z c= K & x in Intersect Z holds
Intersect Z meets {y}
proof
let Z be finite Subset-Family of (product J); ::_thesis: ( Z c= K & x in Intersect Z implies Intersect Z meets {y} )
assume that
A16: Z c= K and
A17: x in Intersect Z ; ::_thesis: Intersect Z meets {y}
 for Y being set st Y in Z holds
y in Y
proof
let Y be set ; ::_thesis: ( Y in Z implies y in Y )
 y in the carrier of (product J) ;
then  y in product (Carrier J) by WAYBEL18:def_3;
then consider g being Function such that
A18: y = g and
A19: dom g = dom (Carrier J) and
A20: for z being set st z in dom (Carrier J) holds
g . z in (Carrier J) . z by CARD_3:def_5;
assume A21: Y in Z ; ::_thesis: y in Y
then  Y in K by A16;
then consider i being set , W being TopStruct , V being Subset of W such that
A22: i in M and
A23: V is open and
A24: W = J . i and
A25: Y = product ((Carrier J) +* (i,V)) by WAYBEL18:def_2;
reconsider i = i as Element of M by A22;
reconsider V = V as Subset of (J . i) by A24;
 x in Y by A17, A21, SETFAM_1:43;
then A26: ex f being Function st
( x = f & dom f = dom ((Carrier J) +* (i,V)) & ( for z being set st z in dom ((Carrier J) +* (i,V)) holds
f . z in ((Carrier J) +* (i,V)) . z ) ) by A25, CARD_3:def_5;
 x . i in Cl {(y . i)} by A15;
then A27: ( x . i in V implies {(y . i)} meets V ) by A23, A24, PRE_TOPC:def_7;
A28: for z being set st z in dom ((Carrier J) +* (i,V)) holds
g . z in ((Carrier J) +* (i,V)) . z
proof
let z be set ; ::_thesis: ( z in dom ((Carrier J) +* (i,V)) implies g . z in ((Carrier J) +* (i,V)) . z )
assume A29: z in dom ((Carrier J) +* (i,V)) ; ::_thesis: g . z in ((Carrier J) +* (i,V)) . z
then A30: z in dom (Carrier J) by FUNCT_7:30;
percases ( z = i or z <> i ) ;
supposeA31: z = i ; ::_thesis: g . z in ((Carrier J) +* (i,V)) . z
then  ((Carrier J) +* (i,V)) . z = V by A30, FUNCT_7:31;
hence  g . z in ((Carrier J) +* (i,V)) . z by A27, A26, A18, A29, A31, ZFMISC_1:50; ::_thesis: verum
end;
suppose z <> i ; ::_thesis: g . z in ((Carrier J) +* (i,V)) . z
then  ((Carrier J) +* (i,V)) . z = (Carrier J) . z by FUNCT_7:32;
hence  g . z in ((Carrier J) +* (i,V)) . z by A20, A30; ::_thesis: verum
end;
end;
end;
 dom g = dom ((Carrier J) +* (i,V)) by A19, FUNCT_7:30;
hence  y in Y by A25, A18, A28, CARD_3:def_5; ::_thesis: verum
end;
then  ( y in {y} & y in Intersect Z ) by SETFAM_1:43, TARSKI:def_1;
hence  Intersect Z meets {y} by XBOOLE_0:3; ::_thesis: verum
end;
hence  x in Cl {y} by YELLOW_9:38; ::_thesis: verum
end;

theorem :: YELLOW14:30
for M being non empty set
for T being non empty TopSpace
for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
proof
let M be non empty set ; ::_thesis: for T being non empty TopSpace
for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let T be non empty TopSpace; ::_thesis: for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let x, y be Point of (product (M --> T)); ::_thesis: ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
reconsider J = M --> T as non-Empty TopStruct-yielding ManySortedSet of M ;
reconsider x9 = x, y9 = y as Point of (product J) ;
thus  ( x in Cl {y} implies for i being Element of M holds x . i in Cl {(y . i)} ) ::_thesis: ( ( for i being Element of M holds x . i in Cl {(y . i)} ) implies x in Cl {y} )
proof
assume A1: x in Cl {y} ; ::_thesis: for i being Element of M holds x . i in Cl {(y . i)}
let i be Element of M; ::_thesis: x . i in Cl {(y . i)}
 x9 . i in Cl {(y9 . i)} by A1, Th29;
hence  x . i in Cl {(y . i)} by FUNCOP_1:7; ::_thesis: verum
end;
assume A2: for i being Element of M holds x . i in Cl {(y . i)} ; ::_thesis: x in Cl {y}
 for i being Element of M holds x9 . i in Cl {(y9 . i)}
proof
let i be Element of M; ::_thesis: x9 . i in Cl {(y9 . i)}
 x . i in Cl {(y . i)} by A2;
hence  x9 . i in Cl {(y9 . i)} by FUNCOP_1:7; ::_thesis: verum
end;
hence  x in Cl {y} by Th29; ::_thesis: verum
end;

theorem Th31: :: YELLOW14:31
for M being non empty set
for i being Element of M
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
proof
let M be non empty set ; ::_thesis: for i being Element of M
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
let i be Element of M; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
let x be Point of (product J); ::_thesis: pi ((Cl {x}),i) = Cl {(x . i)}
consider f being set  such that
A1: f in Cl {x} by XBOOLE_0:def_1;
A2: f in the carrier of (product J) by A1;
thus  pi ((Cl {x}),i) c= Cl {(x . i)} :: according to XBOOLE_0:def_10 ::_thesis: Cl {(x . i)} c= pi ((Cl {x}),i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi ((Cl {x}),i) or a in Cl {(x . i)} )
assume  a in pi ((Cl {x}),i) ; ::_thesis: a in Cl {(x . i)}
then  ex f being Function st
( f in Cl {x} & a = f . i ) by CARD_3:def_6;
hence  a in Cl {(x . i)} by Th29; ::_thesis: verum
end;
reconsider f = f as Element of (product J) by A1;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {(x . i)} or a in pi ((Cl {x}),i) )
set y = f +* (i .--> a);
A3: dom (Carrier J) = M by PARTFUN1:def_2;
A4: f in product (Carrier J) by A2, WAYBEL18:def_3;
then A5: dom f = M by A3, CARD_3:9;
A6: dom (i .--> a) = {i} by FUNCOP_1:13;
assume A7: a in Cl {(x . i)} ; ::_thesis: a in pi ((Cl {x}),i)
A8: for m being set st m in dom (Carrier J) holds
(f +* (i .--> a)) . m in (Carrier J) . m
proof
let m be set ; ::_thesis: ( m in dom (Carrier J) implies (f +* (i .--> a)) . m in (Carrier J) . m )
assume A9: m in dom (Carrier J) ; ::_thesis: (f +* (i .--> a)) . m in (Carrier J) . m
then A10: ex R being 1-sorted st
( R = J . m & (Carrier J) . m = the carrier of R ) by PRALG_1:def_13;
percases ( m = i or m <> i ) ;
supposeA11: m = i ; ::_thesis: (f +* (i .--> a)) . m in (Carrier J) . m
then  (f +* (i .--> a)) . m = a by FUNCT_7:94;
hence  (f +* (i .--> a)) . m in (Carrier J) . m by A7, A10, A11; ::_thesis: verum
end;
suppose m <> i ; ::_thesis: (f +* (i .--> a)) . m in (Carrier J) . m
then  not m in dom (i .--> a) by A6, TARSKI:def_1;
then  (f +* (i .--> a)) . m = f . m by FUNCT_4:11;
hence  (f +* (i .--> a)) . m in (Carrier J) . m by A4, A9, CARD_3:9; ::_thesis: verum
end;
end;
end;
dom (f +* (i .--> a)) = (dom f) \/ (dom (i .--> a)) by FUNCT_4:def_1
.= M \/ {i} by A5, FUNCOP_1:13
.= M by ZFMISC_1:40 ;
then  f +* (i .--> a) in product (Carrier J) by A3, A8, CARD_3:9;
then reconsider y = f +* (i .--> a) as Element of (product J) by WAYBEL18:def_3;
 for m being Element of M holds y . m in Cl {(x . m)}
proof
let m be Element of M; ::_thesis: y . m in Cl {(x . m)}
percases ( m = i or m <> i ) ;
suppose m = i ; ::_thesis: y . m in Cl {(x . m)}
hence  y . m in Cl {(x . m)} by A7, FUNCT_7:94; ::_thesis: verum
end;
suppose m <> i ; ::_thesis: y . m in Cl {(x . m)}
then  not m in dom (i .--> a) by A6, TARSKI:def_1;
then  y . m = f . m by FUNCT_4:11;
hence  y . m in Cl {(x . m)} by A1, Th29; ::_thesis: verum
end;
end;
end;
then A12: f +* (i .--> a) in Cl {x} by Th29;
 (f +* (i .--> a)) . i = a by FUNCT_7:94;
hence  a in pi ((Cl {x}),i) by A12, CARD_3:def_6; ::_thesis: verum
end;

theorem :: YELLOW14:32
for M being non empty set
for i being Element of M
for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
proof
let M be non empty set ; ::_thesis: for i being Element of M
for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
let i be Element of M; ::_thesis: for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
let T be non empty TopSpace; ::_thesis: for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
let x be Point of (product (M --> T)); ::_thesis: pi ((Cl {x}),i) = Cl {(x . i)}
 (M --> T) . i = T by FUNCOP_1:7;
hence  pi ((Cl {x}),i) = Cl {(x . i)} by Th31; ::_thesis: verum
end;

theorem :: YELLOW14:33
for X, Y being non empty TopStruct
for f being Function of X,Y
for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
proof
let X, Y be non empty TopStruct ; ::_thesis: for f being Function of X,Y
for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
let f be Function of X,Y; ::_thesis: for g being Function of Y,X st f = id X & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
let g be Function of Y,X; ::_thesis: ( f = id X & g = id X & f is continuous & g is continuous implies TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) )
assume that
A1: f = id X and
A2: g = id X and
A3: f is continuous and
A4: g is continuous ; ::_thesis: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
A5: the carrier of X = dom f by FUNCT_2:def_1
.= the carrier of Y by A1, A2, FUNCT_2:def_1 ;
A6: [#] Y <> {} ;
A7: [#] X <> {} ;
 the topology of X = the topology of Y
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the topology of Y c= the topology of X
let A be set ; ::_thesis: ( A in the topology of X implies A in the topology of Y )
assume A8: A in the topology of X ; ::_thesis: A in the topology of Y
then reconsider B = A as Subset of X ;
 B is open by A8, PRE_TOPC:def_2;
then A9: g " B is open by A4, A7, TOPS_2:43;
 g " B = B by A2, FUNCT_2:94;
hence  A in the topology of Y by A9, PRE_TOPC:def_2; ::_thesis: verum
end;
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in the topology of Y or A in the topology of X )
assume A10: A in the topology of Y ; ::_thesis: A in the topology of X
then reconsider B = A as Subset of Y ;
 B is open by A10, PRE_TOPC:def_2;
then A11: f " B is open by A3, A6, TOPS_2:43;
 f " B = B by A1, A5, FUNCT_2:94;
hence  A in the topology of X by A11, PRE_TOPC:def_2; ::_thesis: verum
end;
hence  TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #) by A5; ::_thesis: verum
end;

theorem :: YELLOW14:34
for X, Y being non empty TopSpace
for f being Function of X,Y st corestr f is continuous holds
f is continuous
proof
let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y st corestr f is continuous holds
f is continuous
let f be Function of X,Y; ::_thesis: ( corestr f is continuous implies f is continuous )
assume A1: corestr f is continuous ; ::_thesis: f is continuous
 corestr f = f by WAYBEL18:def_7;
hence  f is continuous by A1, PRE_TOPC:26; ::_thesis: verum
end;

registration
let X be non empty TopSpace;
let Y be non empty SubSpace of X;
cluster incl Y ->  continuous ;
coherence
 incl Y is continuous by TMAP_1:87;
end;

theorem :: YELLOW14:35
for T being non empty TopSpace
for f being Function of T,T st f * f = f holds
(corestr f) * (incl (Image f)) = id (Image f)
proof
let T be non empty TopSpace; ::_thesis: for f being Function of T,T st f * f = f holds
(corestr f) * (incl (Image f)) = id (Image f)
let f be Function of T,T; ::_thesis: ( f * f = f implies (corestr f) * (incl (Image f)) = id (Image f) )
assume A1: f * f = f ; ::_thesis: (corestr f) * (incl (Image f)) = id (Image f)
set cf = corestr f;
set i = incl (Image f);
 for x being set st x in the carrier of (Image f) holds
((corestr f) * (incl (Image f))) . x = (id (Image f)) . x
proof
A2: the carrier of (Image f) c= the carrier of T by BORSUK_1:1;
let x be set ; ::_thesis: ( x in the carrier of (Image f) implies ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x )
assume A3: x in the carrier of (Image f) ; ::_thesis: ((corestr f) * (incl (Image f))) . x = (id (Image f)) . x
 the carrier of (Image f) = rng f by WAYBEL18:9;
then A4: ex y being set st
( y in dom f & f . y = x ) by A3, FUNCT_1:def_3;
thus ((corestr f) * (incl (Image f))) . x = (corestr f) . ((incl (Image f)) . x) by A3, FUNCT_2:15
.= (corestr f) . x by A3, A2, TMAP_1:84
.= f . x by WAYBEL18:def_7
.= x by A1, A4, FUNCT_2:15
.= (id (Image f)) . x by A3, FUNCT_1:18 ; ::_thesis: verum
end;
hence  (corestr f) * (incl (Image f)) = id (Image f) by FUNCT_2:12; ::_thesis: verum
end;

theorem :: YELLOW14:36
for Y being non empty TopSpace
for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism
proof
let Y be non empty TopSpace; ::_thesis: for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism
let W be non empty SubSpace of Y; ::_thesis: corestr (incl W) is being_homeomorphism
set ci = corestr (incl W);
thus  dom (corestr (incl W)) = [#] W by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng (corestr (incl W)) = [#] (Image (incl W)) & corestr (incl W) is one-to-one & corestr (incl W) is continuous & (corestr (incl W)) /" is continuous )
thus A1: rng (corestr (incl W)) = [#] (Image (incl W)) by FUNCT_2:def_3; ::_thesis: ( corestr (incl W) is one-to-one & corestr (incl W) is continuous & (corestr (incl W)) /" is continuous )
A2: corestr (incl W) = incl W by WAYBEL18:def_7
.= (id Y) | W by TMAP_1:def_6
.= (id the carrier of Y) | the carrier of W by TMAP_1:def_4 ;
hence A3: corestr (incl W) is V14() by FUNCT_1:52; ::_thesis: ( corestr (incl W) is continuous & (corestr (incl W)) /" is continuous )
A4: for P being Subset of W st P is open holds
((corestr (incl W)) /") " P is open
proof
let P be Subset of W; ::_thesis: ( P is open implies ((corestr (incl W)) /") " P is open )
assume  P in the topology of W ; :: according to PRE_TOPC:def_2 ::_thesis: ((corestr (incl W)) /") " P is open
then A5: ex Q being Subset of Y st
( Q in the topology of Y & P = Q /\ ([#] W) ) by PRE_TOPC:def_4;
A6: the carrier of W is non empty Subset of Y by BORSUK_1:1;
then A7: P is Subset of Y by XBOOLE_1:1;
A8: [#] W = rng ((id the carrier of Y) | the carrier of W) by A6, Th2
.= rng ((id Y) | W) by TMAP_1:def_4
.= rng (incl W) by TMAP_1:def_6
.= [#] (Image (incl W)) by WAYBEL18:9 ;
((corestr (incl W)) /") " P = ((id the carrier of Y) | the carrier of W) .: P by A1, A2, A3, TOPS_2:54
.= (id the carrier of Y) .: P by FUNCT_2:97
.= P by A7, FUNCT_1:92 ;
hence  ((corestr (incl W)) /") " P in the topology of (Image (incl W)) by A5, A8, PRE_TOPC:def_4; :: according to PRE_TOPC:def_2 ::_thesis: verum
end;
thus  corestr (incl W) is continuous by WAYBEL18:10; ::_thesis: (corestr (incl W)) /" is continuous
 [#] W <> {} ;
hence  (corestr (incl W)) /" is continuous by A4, TOPS_2:43; ::_thesis: verum
end;

theorem Th37: :: YELLOW14:37
for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds
product J is T_0
proof
let M be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds
product J is T_0
let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: ( ( for i being Element of M holds J . i is T_0 TopSpace ) implies product J is T_0 )
assume A1: for i being Element of M holds J . i is T_0 TopSpace ; ::_thesis: product J is T_0
 for x, y being Point of (product J) st x <> y holds
Cl {x} <> Cl {y}
proof
let x, y be Point of (product J); ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
assume that
A2: x <> y and
A3: Cl {x} = Cl {y} ; ::_thesis: contradiction
 y in the carrier of (product J) ;
then  y in product (Carrier J) by WAYBEL18:def_3;
then  dom y = dom (Carrier J) by CARD_3:9;
then A4: dom y = M by PARTFUN1:def_2;
 x in the carrier of (product J) ;
then  x in product (Carrier J) by WAYBEL18:def_3;
then  dom x = dom (Carrier J) by CARD_3:9;
then  dom x = M by PARTFUN1:def_2;
then consider i being set  such that
A5: i in M and
A6: x . i <> y . i by A2, A4, FUNCT_1:2;
reconsider i = i as Element of M by A5;
A7: pi ((Cl {y}),i) = Cl {(y . i)} by Th31;
 ( J . i is T_0 TopSpace & pi ((Cl {x}),i) = Cl {(x . i)} ) by A1, Th31;
hence  contradiction by A3, A6, A7, TSP_1:def_5; ::_thesis: verum
end;
hence  product J is T_0 by TSP_1:def_5; ::_thesis: verum
end;

registration
let I be non empty set ;
let T be non empty T_0 TopSpace;
cluster product (I --> T) ->  T_0 ;
coherence
 product (I --> T) is T_0
proof
 for i being Element of I holds (I --> T) . i is T_0 TopSpace by FUNCOP_1:7;
hence  product (I --> T) is T_0 by Th37; ::_thesis: verum
end;
end;

theorem Th38: :: YELLOW14:38
for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds
( J . i is T_1 & J . i is TopSpace-like ) ) holds
product J is T_1
proof
let M be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds
( J . i is T_1 & J . i is TopSpace-like ) ) holds
product J is T_1
let J be non-Empty TopStruct-yielding ManySortedSet of M; ::_thesis: ( ( for i being Element of M holds
( J . i is T_1 & J . i is TopSpace-like ) ) implies product J is T_1 )
assume A1: for i being Element of M holds
( J . i is T_1 & J . i is TopSpace-like ) ; ::_thesis: product J is T_1
 for p being Point of (product J) holds {p} is closed
proof
let p be Point of (product J); ::_thesis: {p} is closed
 {p} = Cl {p}
proof
thus  {p} c= Cl {p} by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl {p} c= {p}
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {p} or a in {p} )
assume A2: a in Cl {p} ; ::_thesis: a in {p}
then reconsider a = a, p = p as Element of (product J) ;
A3: for i being set st i in M holds
a . i = p . i
proof
let i be set ; ::_thesis: ( i in M implies a . i = p . i )
assume  i in M ; ::_thesis: a . i = p . i
then reconsider i = i as Element of M ;
 ( J . i is TopSpace & J . i is T_1 ) by A1;
then A4: {(p . i)} is closed by URYSOHN1:19;
 a . i in Cl {(p . i)} by A2, Th29;
then  a . i in {(p . i)} by A4, PRE_TOPC:22;
hence  a . i = p . i by TARSKI:def_1; ::_thesis: verum
end;
 p in the carrier of (product J) ;
then  p in product (Carrier J) by WAYBEL18:def_3;
then  dom p = dom (Carrier J) by CARD_3:9;
then A5: dom p = M by PARTFUN1:def_2;
 a in the carrier of (product J) ;
then  a in product (Carrier J) by WAYBEL18:def_3;
then  dom a = dom (Carrier J) by CARD_3:9;
then  dom a = M by PARTFUN1:def_2;
then  a = p by A5, A3, FUNCT_1:2;
hence  a in {p} by TARSKI:def_1; ::_thesis: verum
end;
hence  {p} is closed ; ::_thesis: verum
end;
hence  product J is T_1 by URYSOHN1:19; ::_thesis: verum
end;

registration
let I be non empty set ;
let T be non empty T_1 TopSpace;
cluster product (I --> T) ->  T_1 ;
coherence
 product (I --> T) is T_1
proof
 for i being Element of I holds
( (I --> T) . i is T_1 & (I --> T) . i is TopSpace-like ) by FUNCOP_1:7;
hence  product (I --> T) is T_1 by Th38; ::_thesis: verum
end;
end;