:: WAYBEL26 semantic presentation

begin

notation
let I be set ;
let J be RelStr-yielding ManySortedSet of I;
synonym I -POS_prod J for  product J;
end;

notation
let I be set ;
let J be non-Empty TopStruct-yielding ManySortedSet of I;
synonym I -TOP_prod J for  product J;
end;

definition
let X, Y be non empty TopSpace;
func oContMaps (X,Y) ->  non empty strict RelStr  equals :: WAYBEL26:def 1
 ContMaps (X,(Omega Y));
coherence
 ContMaps (X,(Omega Y)) is non empty strict RelStr ;
end;

:: deftheorem  defines oContMaps WAYBEL26:def_1_:_
 for X, Y being non empty TopSpace holds oContMaps (X,Y) = ContMaps (X,(Omega Y));

registration
let X, Y be non empty TopSpace;
cluster oContMaps (X,Y) ->  non empty constituted-Functions strict reflexive transitive ;
coherence
 ( oContMaps (X,Y) is reflexive & oContMaps (X,Y) is transitive & oContMaps (X,Y) is constituted-Functions ) ;
end;

registration
let X be non empty TopSpace;
let Y be non empty T_0 TopSpace;
cluster oContMaps (X,Y) ->  non empty strict antisymmetric ;
coherence
 oContMaps (X,Y) is antisymmetric ;
end;

theorem Th1: :: WAYBEL26:1
for X, Y being non empty TopSpace
for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )
proof
let X, Y be non empty TopSpace; ::_thesis: for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )
let a be set ; ::_thesis: ( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,(Omega Y) )
hereby  ::_thesis: ( a is continuous Function of X,(Omega Y) implies a is Element of (oContMaps (X,Y)) )
assume  a is Element of (oContMaps (X,Y)) ; ::_thesis: a is continuous Function of X,(Omega Y)
then  ex f being Function of X,(Omega Y) st
( a = f & f is continuous ) by WAYBEL24:def_3;
hence  a is continuous Function of X,(Omega Y) ; ::_thesis: verum
end;
assume  a is continuous Function of X,(Omega Y) ; ::_thesis: a is Element of (oContMaps (X,Y))
hence  a is Element of (oContMaps (X,Y)) by WAYBEL24:def_3; ::_thesis: verum
end;

theorem Th2: :: WAYBEL26:2
for X, Y being non empty TopSpace
for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,Y )
proof
let X, Y be non empty TopSpace; ::_thesis: for a being set holds
( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,Y )
let a be set ; ::_thesis: ( a is Element of (oContMaps (X,Y)) iff a is continuous Function of X,Y )
A1: ( TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) & TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of X, the topology of X #) ) by WAYBEL25:def_2;
hereby  ::_thesis: ( a is continuous Function of X,Y implies a is Element of (oContMaps (X,Y)) )
assume  a is Element of (oContMaps (X,Y)) ; ::_thesis: a is continuous Function of X,Y
then  a is continuous Function of X,(Omega Y) by Th1;
hence  a is continuous Function of X,Y by A1, YELLOW12:36; ::_thesis: verum
end;
assume  a is continuous Function of X,Y ; ::_thesis: a is Element of (oContMaps (X,Y))
then  a is continuous Function of X,(Omega Y) by A1, YELLOW12:36;
hence  a is Element of (oContMaps (X,Y)) by Th1; ::_thesis: verum
end;

theorem Th3: :: WAYBEL26:3
for X, Y being non empty TopSpace
for a, b being Element of (oContMaps (X,Y))
for f, g being Function of X,(Omega Y) st a = f & b = g holds
( a <= b iff f <= g )
proof
let X, Y be non empty TopSpace; ::_thesis: for a, b being Element of (oContMaps (X,Y))
for f, g being Function of X,(Omega Y) st a = f & b = g holds
( a <= b iff f <= g )
let a, b be Element of (oContMaps (X,Y)); ::_thesis: for f, g being Function of X,(Omega Y) st a = f & b = g holds
( a <= b iff f <= g )
A1: oContMaps (X,Y) is full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then reconsider x = a, y = b as Element of ((Omega Y) |^ the carrier of X) by YELLOW_0:58;
A2: ( a <= b iff x <= y ) by A1, YELLOW_0:59, YELLOW_0:60;
let f, g be Function of X,(Omega Y); ::_thesis: ( a = f & b = g implies ( a <= b iff f <= g ) )
assume  ( a = f & b = g ) ; ::_thesis: ( a <= b iff f <= g )
hence  ( a <= b iff f <= g ) by A2, WAYBEL10:11; ::_thesis: verum
end;

definition
let X, Y be non empty TopSpace;
let x be Point of X;
let A be Subset of (oContMaps (X,Y));
:: original: pi
redefine func pi (A,x) ->  Subset of (Omega Y);
coherence
 pi (A,x) is Subset of (Omega Y)
proof
set XY = oContMaps (X,Y);
 oContMaps (X,Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then  the carrier of (oContMaps (X,Y)) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
then reconsider A = A as Subset of ((Omega Y) |^ the carrier of X) by XBOOLE_1:1;
 pi (A,x) is Subset of (Omega Y) ;
hence  pi (A,x) is Subset of (Omega Y) ; ::_thesis: verum
end;
end;

registration
let X, Y be non empty TopSpace;
let x be set ;
let A be non empty Subset of (oContMaps (X,Y));
cluster pi (A,x) ->  non empty ;
coherence
 not pi (A,x) is empty
proof
set XY = oContMaps (X,Y);
 oContMaps (X,Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then  the carrier of (oContMaps (X,Y)) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
then reconsider A = A as non empty Subset of ((Omega Y) |^ the carrier of X) by XBOOLE_1:1;
 pi (A,x) <> {} ;
hence  not pi (A,x) is empty ; ::_thesis: verum
end;
end;

theorem Th4: :: WAYBEL26:4
Omega Sierpinski_Space is TopAugmentation of BoolePoset 1
proof
set S = the strict Scott TopAugmentation of BoolePoset 1;
A1: RelStr(# the carrier of the strict Scott TopAugmentation of BoolePoset 1, the InternalRel of the strict Scott TopAugmentation of BoolePoset 1 #) = BoolePoset 1 by YELLOW_9:def_4;
 BoolePoset 1 = InclPoset (bool 1) by YELLOW_1:4;
then A2: the carrier of (BoolePoset 1) = {0,1} by YELLOW14:1, YELLOW_1:1;
 ( the carrier of Sierpinski_Space = {0,1} & the topology of the strict Scott TopAugmentation of BoolePoset 1 = the topology of Sierpinski_Space ) by WAYBEL18:12, WAYBEL18:def_9;
then  Omega Sierpinski_Space = Omega the strict Scott TopAugmentation of BoolePoset 1 by A2, A1, WAYBEL25:13
.= the strict Scott TopAugmentation of BoolePoset 1 by WAYBEL25:15 ;
hence  Omega Sierpinski_Space is TopAugmentation of BoolePoset 1 ; ::_thesis: verum
end;

theorem Th5: :: WAYBEL26:5
for X being non empty TopSpace ex f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) st
( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )
proof
let X be non empty TopSpace; ::_thesis: ex f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) st
( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )
deffunc H1( set ) ->  Element of bool [: the carrier of X,{{},1}:] = chi ($1, the carrier of X);
consider f being Function such that
A1: dom f = the topology of X and
A2: for a being set st a in the topology of X holds
f . a = H1(a) from FUNCT_1:sch_3();
A3: rng f c= the carrier of (oContMaps (X,Sierpinski_Space))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in the carrier of (oContMaps (X,Sierpinski_Space)) )
assume  x in rng f ; ::_thesis: x in the carrier of (oContMaps (X,Sierpinski_Space))
then consider a being set  such that
A4: a in dom f and
A5: x = f . a by FUNCT_1:def_3;
reconsider a = a as Subset of X by A1, A4;
 a is open by A1, A4, PRE_TOPC:def_2;
then  chi (a, the carrier of X) is continuous Function of X,Sierpinski_Space by YELLOW16:46;
then  x is continuous Function of X,Sierpinski_Space by A1, A2, A4, A5;
then  x is Element of (oContMaps (X,Sierpinski_Space)) by Th2;
hence  x in the carrier of (oContMaps (X,Sierpinski_Space)) ; ::_thesis: verum
end;
set S = InclPoset the topology of X;
A6: the carrier of (InclPoset the topology of X) = the topology of X by YELLOW_1:1;
then reconsider f = f as Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) by A1, A3, FUNCT_2:2;
A7: now__::_thesis:_for_x,_y_being_Element_of_(InclPoset_the_topology_of_X)_holds_
(_x_<=_y_iff_f_._x_<=_f_._y_)
let x, y be Element of (InclPoset the topology of X); ::_thesis: ( x <= y iff f . x <= f . y )
 ( x in the topology of X & y in the topology of X ) by A6;
then reconsider V = x, W = y as open Subset of X by PRE_TOPC:def_2;
set cx = chi (V, the carrier of X);
set cy = chi (W, the carrier of X);
A8: ( f . x = chi (V, the carrier of X) & f . y = chi (W, the carrier of X) ) by A2, A6;
 chi (V, the carrier of X) is continuous Function of X,Sierpinski_Space by YELLOW16:46;
then A9: chi (V, the carrier of X) is Element of (oContMaps (X,Sierpinski_Space)) by Th2;
 chi (W, the carrier of X) is continuous Function of X,Sierpinski_Space by YELLOW16:46;
then  chi (W, the carrier of X) is Element of (oContMaps (X,Sierpinski_Space)) by Th2;
then reconsider cx = chi (V, the carrier of X), cy = chi (W, the carrier of X) as continuous Function of X,(Omega Sierpinski_Space) by A9, Th1;
 ( x <= y iff V c= W ) by YELLOW_1:3;
then  ( x <= y iff cx <= cy ) by Th4, YELLOW16:49;
hence  ( x <= y iff f . x <= f . y ) by A8, Th3; ::_thesis: verum
end;
set T = oContMaps (X,Sierpinski_Space);
A10: rng f = the carrier of (oContMaps (X,Sierpinski_Space))
proof
 the topology of Sierpinski_Space = {{},{1},{0,1}} by WAYBEL18:def_9;
then  {1} in the topology of Sierpinski_Space by ENUMSET1:def_1;
then reconsider V = {1} as open Subset of Sierpinski_Space by PRE_TOPC:def_2;
thus  rng f c= the carrier of (oContMaps (X,Sierpinski_Space)) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (oContMaps (X,Sierpinski_Space)) c= rng f
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in the carrier of (oContMaps (X,Sierpinski_Space)) or t in rng f )
assume  t in the carrier of (oContMaps (X,Sierpinski_Space)) ; ::_thesis: t in rng f
then reconsider g = t as continuous Function of X,Sierpinski_Space by Th2;
 [#] Sierpinski_Space <> {} ;
then A11: g " V is open by TOPS_2:43;
then reconsider c = chi ((g " V), the carrier of X) as Function of X,Sierpinski_Space by YELLOW16:46;
now__::_thesis:_for_x_being_Element_of_X_holds_g_._x_=_c_._x
let x be Element of X; ::_thesis: g . x = c . x
 ( x in g " V or not x in g " V ) ;
then A12: ( ( g . x in V & c . x = 1 ) or ( not g . x in V & c . x = 0 ) ) by FUNCT_2:38, FUNCT_3:def_3;
 the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9;
then  ( g . x = 0 or g . x = 1 ) by TARSKI:def_2;
hence  g . x = c . x by A12, TARSKI:def_1; ::_thesis: verum
end;
then A13: g = c by FUNCT_2:63;
A14: g " V in the topology of X by A11, PRE_TOPC:def_2;
then  f . (g " V) = chi ((g " V), the carrier of X) by A2;
hence  t in rng f by A1, A14, A13, FUNCT_1:def_3; ::_thesis: verum
end;
take  f ; ::_thesis: ( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )
 f is V7()
proof
let x, y be Element of (InclPoset the topology of X); :: according to WAYBEL_1:def_1 ::_thesis: ( not f . x = f . y or x = y )
 ( x in the topology of X & y in the topology of X ) by A6;
then reconsider V = x, W = y as Subset of X ;
 ( f . x = chi (V, the carrier of X) & f . y = chi (W, the carrier of X) ) by A2, A6;
hence  ( not f . x = f . y or x = y ) by FUNCT_3:38; ::_thesis: verum
end;
hence  f is isomorphic by A10, A7, WAYBEL_0:66; ::_thesis: for V being open Subset of X holds f . V = chi (V, the carrier of X)
let V be open Subset of X; ::_thesis: f . V = chi (V, the carrier of X)
 V in the topology of X by PRE_TOPC:def_2;
hence  f . V = chi (V, the carrier of X) by A2; ::_thesis: verum
end;

theorem Th6: :: WAYBEL26:6
for X being non empty TopSpace holds InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic
proof
let X be non empty TopSpace; ::_thesis: InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic
consider f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) such that
A1: f is isomorphic and
 for V being open Subset of X holds f . V = chi (V, the carrier of X) by Th5;
take  f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic
thus  f is isomorphic by A1; ::_thesis: verum
end;

definition
let X, Y, Z be non empty TopSpace;
let f be continuous Function of Y,Z;
func oContMaps (X,f) ->  Function of (oContMaps (X,Y)),(oContMaps (X,Z)) means :Def2: :: WAYBEL26:def 2
 for g being continuous Function of X,Y holds it . g = f * g;
uniqueness
 for b1, b2 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st ( for g being continuous Function of X,Y holds b1 . g = f * g ) & ( for g being continuous Function of X,Y holds b2 . g = f * g ) holds
b1 = b2
proof
let G1, G2 be Function of (oContMaps (X,Y)),(oContMaps (X,Z)); ::_thesis: ( ( for g being continuous Function of X,Y holds G1 . g = f * g ) & ( for g being continuous Function of X,Y holds G2 . g = f * g ) implies G1 = G2 )
assume that
A1: for g being continuous Function of X,Y holds G1 . g = f * g and
A2: for g being continuous Function of X,Y holds G2 . g = f * g ; ::_thesis: G1 = G2
now__::_thesis:_(_the_carrier_of_(oContMaps_(X,Z))_<>_{}_&_(_for_x_being_Element_of_(oContMaps_(X,Y))_holds_G1_._x_=_G2_._x_)_)
thus  the carrier of (oContMaps (X,Z)) <> {} ; ::_thesis: for x being Element of (oContMaps (X,Y)) holds G1 . x = G2 . x
let x be Element of (oContMaps (X,Y)); ::_thesis: G1 . x = G2 . x
reconsider g = x as continuous Function of X,Y by Th2;
thus G1 . x = f * g by A1
.= G2 . x by A2 ; ::_thesis: verum
end;
hence  G1 = G2 by FUNCT_2:63; ::_thesis: verum
end;
existence
 ex b1 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st
for g being continuous Function of X,Y holds b1 . g = f * g
proof
deffunc H1( set ) ->  set = $1 (#) f;
consider F being Function such that
A3: dom F = the carrier of (oContMaps (X,Y)) and
A4: for x being set st x in the carrier of (oContMaps (X,Y)) holds
F . x = H1(x) from FUNCT_1:sch_3();
 rng F c= the carrier of (oContMaps (X,Z))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of (oContMaps (X,Z)) )
assume  y in rng F ; ::_thesis: y in the carrier of (oContMaps (X,Z))
then consider x being set  such that
A5: x in dom F and
A6: y = F . x by FUNCT_1:def_3;
reconsider g = x as continuous Function of X,Y by A3, A5, Th2;
y = g (#) f by A3, A4, A5, A6
.= f * g ;
then  y is Element of (oContMaps (X,Z)) by Th2;
hence  y in the carrier of (oContMaps (X,Z)) ; ::_thesis: verum
end;
then reconsider F = F as Function of (oContMaps (X,Y)),(oContMaps (X,Z)) by A3, FUNCT_2:2;
take  F ; ::_thesis: for g being continuous Function of X,Y holds F . g = f * g
let g be continuous Function of X,Y; ::_thesis: F . g = f * g
 g is Element of (oContMaps (X,Y)) by Th2;
hence F . g = g (#) f by A4
.= f * g ;
::_thesis: verum
end;
func oContMaps (f,X) ->  Function of (oContMaps (Z,X)),(oContMaps (Y,X)) means :Def3: :: WAYBEL26:def 3
 for g being continuous Function of Z,X holds it . g = g * f;
uniqueness
 for b1, b2 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st ( for g being continuous Function of Z,X holds b1 . g = g * f ) & ( for g being continuous Function of Z,X holds b2 . g = g * f ) holds
b1 = b2
proof
let G1, G2 be Function of (oContMaps (Z,X)),(oContMaps (Y,X)); ::_thesis: ( ( for g being continuous Function of Z,X holds G1 . g = g * f ) & ( for g being continuous Function of Z,X holds G2 . g = g * f ) implies G1 = G2 )
assume that
A7: for g being continuous Function of Z,X holds G1 . g = g * f and
A8: for g being continuous Function of Z,X holds G2 . g = g * f ; ::_thesis: G1 = G2
now__::_thesis:_(_the_carrier_of_(oContMaps_(Y,X))_<>_{}_&_(_for_x_being_Element_of_(oContMaps_(Z,X))_holds_G1_._x_=_G2_._x_)_)
thus  the carrier of (oContMaps (Y,X)) <> {} ; ::_thesis: for x being Element of (oContMaps (Z,X)) holds G1 . x = G2 . x
let x be Element of (oContMaps (Z,X)); ::_thesis: G1 . x = G2 . x
reconsider g = x as continuous Function of Z,X by Th2;
thus G1 . x = g * f by A7
.= G2 . x by A8 ; ::_thesis: verum
end;
hence  G1 = G2 by FUNCT_2:63; ::_thesis: verum
end;
existence
 ex b1 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st
for g being continuous Function of Z,X holds b1 . g = g * f
proof
deffunc H1( set ) ->  set = f (#) $1;
consider F being Function such that
A9: dom F = the carrier of (oContMaps (Z,X)) and
A10: for x being set st x in the carrier of (oContMaps (Z,X)) holds
F . x = H1(x) from FUNCT_1:sch_3();
 rng F c= the carrier of (oContMaps (Y,X))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of (oContMaps (Y,X)) )
assume  y in rng F ; ::_thesis: y in the carrier of (oContMaps (Y,X))
then consider x being set  such that
A11: x in dom F and
A12: y = F . x by FUNCT_1:def_3;
reconsider g = x as continuous Function of Z,X by A9, A11, Th2;
y = f (#) g by A9, A10, A11, A12
.= g * f ;
then  y is Element of (oContMaps (Y,X)) by Th2;
hence  y in the carrier of (oContMaps (Y,X)) ; ::_thesis: verum
end;
then reconsider F = F as Function of (oContMaps (Z,X)),(oContMaps (Y,X)) by A9, FUNCT_2:2;
take  F ; ::_thesis: for g being continuous Function of Z,X holds F . g = g * f
let g be continuous Function of Z,X; ::_thesis: F . g = g * f
 g is Element of (oContMaps (Z,X)) by Th2;
hence F . g = f (#) g by A10
.= g * f ;
::_thesis: verum
end;
end;

:: deftheorem Def2 defines oContMaps WAYBEL26:def_2_:_
 for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for b5 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) holds
( b5 = oContMaps (X,f) iff for g being continuous Function of X,Y holds b5 . g = f * g );

:: deftheorem Def3 defines oContMaps WAYBEL26:def_3_:_
 for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for b5 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) holds
( b5 = oContMaps (f,X) iff for g being continuous Function of Z,X holds b5 . g = g * f );

theorem Th7: :: WAYBEL26:7
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace holds oContMaps (X,Y) is up-complete
proof
let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace holds oContMaps (X,Y) is up-complete
let Y be monotone-convergence T_0-TopSpace; ::_thesis: oContMaps (X,Y) is up-complete
 ContMaps (X,(Omega Y)) is full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3, WAYBEL25:43;
hence  oContMaps (X,Y) is up-complete by YELLOW16:5; ::_thesis: verum
end;

theorem Th8: :: WAYBEL26:8
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z holds oContMaps (X,f) is monotone
proof
let X, Y, Z be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Z holds oContMaps (X,f) is monotone
let f be continuous Function of Y,Z; ::_thesis: oContMaps (X,f) is monotone
let a, b be Element of (oContMaps (X,Y)); :: according to WAYBEL_1:def_2 ::_thesis: ( not a <= b or (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b )
 ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) & TopStruct(# the carrier of Z, the topology of Z #) = TopStruct(# the carrier of (Omega Z), the topology of (Omega Z) #) ) by WAYBEL25:def_2;
then reconsider f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;
reconsider g1 = a, g2 = b as continuous Function of X,(Omega Y) by Th1;
set Xf = oContMaps (X,f);
reconsider fg1 = f9 * g1, fg2 = f9 * g2 as Function of X,(Omega Z) ;
 g2 is continuous Function of X,Y by Th2;
then A1: (oContMaps (X,f)) . b = f9 * g2 by Def2;
assume  a <= b ; ::_thesis: (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b
then A2: g1 <= g2 by Th3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_X_holds_
ex_a,_b_being_Element_of_(Omega_Z)_st_
(_a_=_(f9_*_g1)_._x_&_b_=_(f9_*_g2)_._x_&_a_<=_b_)
let x be set ; ::_thesis: ( x in the carrier of X implies ex a, b being Element of (Omega Z) st
( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b ) )
assume  x in the carrier of X ; ::_thesis: ex a, b being Element of (Omega Z) st
( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b )
then reconsider x9 = x as Element of X ;
A3: (f9 * g2) . x9 = f9 . (g2 . x9) by FUNCT_2:15;
 ( ex a, b being Element of (Omega Y) st
( a = g1 . x9 & b = g2 . x9 & a <= b ) & (f9 * g1) . x9 = f9 . (g1 . x9) ) by A2, FUNCT_2:15, YELLOW_2:def_1;
then  (f9 * g1) . x9 <= (f9 * g2) . x9 by A3, WAYBEL_1:def_2;
hence  ex a, b being Element of (Omega Z) st
( a = (f9 * g1) . x & b = (f9 * g2) . x & a <= b ) ; ::_thesis: verum
end;
then A4: fg1 <= fg2 by YELLOW_2:def_1;
 g1 is continuous Function of X,Y by Th2;
then  (oContMaps (X,f)) . a = f9 * g1 by Def2;
hence  (oContMaps (X,f)) . a <= (oContMaps (X,f)) . b by A1, A4, Th3; ::_thesis: verum
end;

theorem :: WAYBEL26:9
for X, Y being non empty TopSpace
for f being continuous Function of Y,Y st f is idempotent holds
oContMaps (X,f) is idempotent
proof
let X, Y be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Y st f is idempotent holds
oContMaps (X,f) is idempotent
let f be continuous Function of Y,Y; ::_thesis: ( f is idempotent implies oContMaps (X,f) is idempotent )
assume A1: f is idempotent ; ::_thesis: oContMaps (X,f) is idempotent
set Xf = oContMaps (X,f);
now__::_thesis:_for_g_being_Element_of_(oContMaps_(X,Y))_holds_((oContMaps_(X,f))_*_(oContMaps_(X,f)))_._g_=_(oContMaps_(X,f))_._g
let g be Element of (oContMaps (X,Y)); ::_thesis: ((oContMaps (X,f)) * (oContMaps (X,f))) . g = (oContMaps (X,f)) . g
reconsider h = g as continuous Function of X,Y by Th2;
thus ((oContMaps (X,f)) * (oContMaps (X,f))) . g = (oContMaps (X,f)) . ((oContMaps (X,f)) . g) by FUNCT_2:15
.= (oContMaps (X,f)) . (f * h) by Def2
.= f * (f * h) by Def2
.= (f * f) * h by RELAT_1:36
.= f * h by A1, QUANTAL1:def_9
.= (oContMaps (X,f)) . g by Def2 ; ::_thesis: verum
end;
then  (oContMaps (X,f)) * (oContMaps (X,f)) = oContMaps (X,f) by FUNCT_2:63;
hence  oContMaps (X,f) is idempotent by QUANTAL1:def_9; ::_thesis: verum
end;

theorem Th10: :: WAYBEL26:10
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z holds oContMaps (f,X) is monotone
proof
let X, Y, Z be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Z holds oContMaps (f,X) is monotone
let f be continuous Function of Y,Z; ::_thesis: oContMaps (f,X) is monotone
let a, b be Element of (oContMaps (Z,X)); :: according to WAYBEL_1:def_2 ::_thesis: ( not a <= b or (oContMaps (f,X)) . a <= (oContMaps (f,X)) . b )
reconsider g1 = a, g2 = b as continuous Function of Z,(Omega X) by Th1;
set Xf = oContMaps (f,X);
 ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) & TopStruct(# the carrier of Z, the topology of Z #) = TopStruct(# the carrier of (Omega Z), the topology of (Omega Z) #) ) by WAYBEL25:def_2;
then reconsider f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;
 g2 is continuous Function of Z,X by Th2;
then A1: (oContMaps (f,X)) . b = g2 * f9 by Def3;
 g1 is continuous Function of Z,X by Th2;
then A2: (oContMaps (f,X)) . a = g1 * f9 by Def3;
then reconsider fg1 = g1 * f9, fg2 = g2 * f9 as Function of Y,(Omega X) by A1, Th1;
assume  a <= b ; ::_thesis: (oContMaps (f,X)) . a <= (oContMaps (f,X)) . b
then A3: g1 <= g2 by Th3;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_Y_holds_
ex_a,_b_being_Element_of_(Omega_X)_st_
(_a_=_(g1_*_f)_._x_&_b_=_(g2_*_f)_._x_&_a_<=_b_)
let x be set ; ::_thesis: ( x in the carrier of Y implies ex a, b being Element of (Omega X) st
( a = (g1 * f) . x & b = (g2 * f) . x & a <= b ) )
assume  x in the carrier of Y ; ::_thesis: ex a, b being Element of (Omega X) st
( a = (g1 * f) . x & b = (g2 * f) . x & a <= b )
then reconsider x9 = x as Element of Y ;
 ( (g1 * f) . x9 = g1 . (f . x9) & (g2 * f) . x9 = g2 . (f . x9) ) by FUNCT_2:15;
hence  ex a, b being Element of (Omega X) st
( a = (g1 * f) . x & b = (g2 * f) . x & a <= b ) by A3, YELLOW_2:def_1; ::_thesis: verum
end;
then  fg1 <= fg2 by YELLOW_2:def_1;
hence  (oContMaps (f,X)) . a <= (oContMaps (f,X)) . b by A2, A1, Th3; ::_thesis: verum
end;

theorem Th11: :: WAYBEL26:11
for X, Y being non empty TopSpace
for f being continuous Function of Y,Y st f is idempotent holds
oContMaps (f,X) is idempotent
proof
let X, Y be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Y st f is idempotent holds
oContMaps (f,X) is idempotent
let f be continuous Function of Y,Y; ::_thesis: ( f is idempotent implies oContMaps (f,X) is idempotent )
assume A1: f is idempotent ; ::_thesis: oContMaps (f,X) is idempotent
set fX = oContMaps (f,X);
now__::_thesis:_for_g_being_Element_of_(oContMaps_(Y,X))_holds_((oContMaps_(f,X))_*_(oContMaps_(f,X)))_._g_=_(oContMaps_(f,X))_._g
let g be Element of (oContMaps (Y,X)); ::_thesis: ((oContMaps (f,X)) * (oContMaps (f,X))) . g = (oContMaps (f,X)) . g
reconsider h = g as continuous Function of Y,X by Th2;
thus ((oContMaps (f,X)) * (oContMaps (f,X))) . g = (oContMaps (f,X)) . ((oContMaps (f,X)) . g) by FUNCT_2:15
.= (oContMaps (f,X)) . (h * f) by Def3
.= (h * f) * f by Def3
.= h * (f * f) by RELAT_1:36
.= h * f by A1, QUANTAL1:def_9
.= (oContMaps (f,X)) . g by Def3 ; ::_thesis: verum
end;
then  (oContMaps (f,X)) * (oContMaps (f,X)) = oContMaps (f,X) by FUNCT_2:63;
hence  oContMaps (f,X) is idempotent by QUANTAL1:def_9; ::_thesis: verum
end;

theorem Th12: :: WAYBEL26:12
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for x being Element of X
for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
proof
let X, Y, Z be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Z
for x being Element of X
for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
let f be continuous Function of Y,Z; ::_thesis: for x being Element of X
for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
set Xf = oContMaps (X,f);
let x be Element of X; ::_thesis: for A being Subset of (oContMaps (X,Y)) holds pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
let A be Subset of (oContMaps (X,Y)); ::_thesis: pi (((oContMaps (X,f)) .: A),x) = f .: (pi (A,x))
thus  pi (((oContMaps (X,f)) .: A),x) c= f .: (pi (A,x)) :: according to XBOOLE_0:def_10 ::_thesis: f .: (pi (A,x)) c= pi (((oContMaps (X,f)) .: A),x)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (((oContMaps (X,f)) .: A),x) or a in f .: (pi (A,x)) )
assume  a in pi (((oContMaps (X,f)) .: A),x) ; ::_thesis: a in f .: (pi (A,x))
then consider h being Function such that
A1: h in (oContMaps (X,f)) .: A and
A2: a = h . x by CARD_3:def_6;
consider g being set  such that
A3: g in the carrier of (oContMaps (X,Y)) and
A4: g in A and
A5: h = (oContMaps (X,f)) . g by A1, FUNCT_2:64;
reconsider g = g as continuous Function of X,Y by A3, Th2;
 h = f * g by A5, Def2;
then A6: a = f . (g . x) by A2, FUNCT_2:15;
 g . x in pi (A,x) by A4, CARD_3:def_6;
hence  a in f .: (pi (A,x)) by A6, FUNCT_2:35; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: (pi (A,x)) or a in pi (((oContMaps (X,f)) .: A),x) )
assume  a in f .: (pi (A,x)) ; ::_thesis: a in pi (((oContMaps (X,f)) .: A),x)
then consider b being set  such that
 b in the carrier of Y and
A7: b in pi (A,x) and
A8: a = f . b by FUNCT_2:64;
consider g being Function such that
A9: g in A and
A10: b = g . x by A7, CARD_3:def_6;
reconsider g = g as continuous Function of X,Y by A9, Th2;
 f * g = (oContMaps (X,f)) . g by Def2;
then A11: f * g in (oContMaps (X,f)) .: A by A9, FUNCT_2:35;
 a = (f * g) . x by A8, A10, FUNCT_2:15;
hence  a in pi (((oContMaps (X,f)) .: A),x) by A11, CARD_3:def_6; ::_thesis: verum
end;

theorem Th13: :: WAYBEL26:13
for X being non empty TopSpace
for Y, Z being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving
proof
let X be non empty TopSpace; ::_thesis: for Y, Z being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving
let Y, Z be monotone-convergence T_0-TopSpace; ::_thesis: for f being continuous Function of Y,Z holds oContMaps (X,f) is directed-sups-preserving
let f be continuous Function of Y,Z; ::_thesis: oContMaps (X,f) is directed-sups-preserving
let A be Subset of (oContMaps (X,Y)); :: according to WAYBEL_0:def_37 ::_thesis: ( A is empty or not A is directed or oContMaps (X,f) preserves_sup_of A )
reconsider sA = sup A as continuous Function of X,Y by Th2;
set Xf = oContMaps (X,f);
reconsider sfA = sup ((oContMaps (X,f)) .: A), XfsA = (oContMaps (X,f)) . (sup A) as Function of X,(Omega Z) by Th1;
reconsider XZ = oContMaps (X,Z) as non empty full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X by WAYBEL24:def_3, WAYBEL25:43;
assume  ( not A is empty & A is directed ) ; ::_thesis: oContMaps (X,f) preserves_sup_of A
then reconsider A9 = A as non empty directed Subset of (oContMaps (X,Y)) ;
reconsider fA9 = (oContMaps (X,f)) .: A9 as non empty directed Subset of (oContMaps (X,Z)) by Th8, YELLOW_2:15;
reconsider XY = oContMaps (X,Y) as non empty full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3, WAYBEL25:43;
reconsider B = A9 as non empty directed Subset of XY ;
reconsider B9 = B as non empty directed Subset of ((Omega Y) |^ the carrier of X) by YELLOW_2:7;
reconsider fB = fA9 as non empty directed Subset of XZ ;
reconsider fB9 = fB as non empty directed Subset of ((Omega Z) |^ the carrier of X) by YELLOW_2:7;
assume  ex_sup_of A, oContMaps (X,Y) ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (oContMaps (X,f)) .: A, oContMaps (X,Z) & "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y)))) )
set I = the carrier of X;
set J1 = the carrier of X --> (Omega Y);
set J2 = the carrier of X --> (Omega Z);
 ( TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) & TopStruct(# the carrier of Z, the topology of Z #) = TopStruct(# the carrier of (Omega Z), the topology of (Omega Z) #) ) by WAYBEL25:def_2;
then reconsider f9 = f as continuous Function of (Omega Y),(Omega Z) by YELLOW12:36;
 ex_sup_of fB9,(Omega Z) |^ the carrier of X by WAYBEL_0:75;
then A1: sup fB9 = sup ((oContMaps (X,f)) .: A) by WAYBEL_0:7;
 ( oContMaps (X,Z) is up-complete & fA9 is directed ) by Th7;
hence  ex_sup_of (oContMaps (X,f)) .: A, oContMaps (X,Z) by WAYBEL_0:75; ::_thesis: "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y))))
A2: (Omega Z) |^ the carrier of X = the carrier of X -POS_prod ( the carrier of X --> (Omega Z)) by YELLOW_1:def_5;
then reconsider fB99 = fB9 as non empty directed Subset of ( the carrier of X -POS_prod ( the carrier of X --> (Omega Z))) ;
now__::_thesis:_for_x_being_Element_of_X_holds_ex_sup_of_pi_(fB99,x),(_the_carrier_of_X_-->_(Omega_Z))_._x
let x be Element of X; ::_thesis: ex_sup_of pi (fB99,x),( the carrier of X --> (Omega Z)) . x
 ( ( the carrier of X --> (Omega Z)) . x = Omega Z & pi (fB99,x) is directed ) by FUNCOP_1:7, YELLOW16:35;
hence  ex_sup_of pi (fB99,x),( the carrier of X --> (Omega Z)) . x by WAYBEL_0:75; ::_thesis: verum
end;
then A3: ex_sup_of fB99, the carrier of X -POS_prod ( the carrier of X --> (Omega Z)) by YELLOW16:31;
A4: (Omega Y) |^ the carrier of X = the carrier of X -POS_prod ( the carrier of X --> (Omega Y)) by YELLOW_1:def_5;
then reconsider B99 = B9 as non empty directed Subset of ( the carrier of X -POS_prod ( the carrier of X --> (Omega Y))) ;
A5: ex_sup_of B9,(Omega Y) |^ the carrier of X by WAYBEL_0:75;
then A6: sup B9 = sup A by WAYBEL_0:7;
now__::_thesis:_for_x_being_Element_of_X_holds_sfA_._x_=_XfsA_._x
let x be Element of X; ::_thesis: sfA . x = XfsA . x
A7: ( the carrier of X --> (Omega Y)) . x = Omega Y by FUNCOP_1:7;
then reconsider Bx = pi (B99,x) as non empty directed Subset of (Omega Y) by YELLOW16:35;
A8: ( ( the carrier of X --> (Omega Z)) . x = Omega Z & ex_sup_of Bx, Omega Y ) by FUNCOP_1:7, WAYBEL_0:75;
A9: (sup B99) . x = sup (pi (B99,x)) by A5, A4, YELLOW16:33;
A10: ( f9 preserves_sup_of Bx & pi (fB99,x) = f9 .: Bx ) by Th12, WAYBEL_0:def_37;
thus sfA . x = sup (pi (fB99,x)) by A1, A2, A3, YELLOW16:33
.= f . (sup Bx) by A8, A10, WAYBEL_0:def_31
.= (f * sA) . x by A6, A4, A9, A7, FUNCT_2:15
.= XfsA . x by Def2 ; ::_thesis: verum
end;
hence  "\/" (((oContMaps (X,f)) .: A),(oContMaps (X,Z))) = (oContMaps (X,f)) . ("\/" (A,(oContMaps (X,Y)))) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th14: :: WAYBEL26:14
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z
for x being Element of Y
for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))
proof
let X, Y, Z be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Z
for x being Element of Y
for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))
let f be continuous Function of Y,Z; ::_thesis: for x being Element of Y
for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))
set fX = oContMaps (f,X);
let x be Element of Y; ::_thesis: for A being Subset of (oContMaps (Z,X)) holds pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))
let A be Subset of (oContMaps (Z,X)); ::_thesis: pi (((oContMaps (f,X)) .: A),x) = pi (A,(f . x))
thus  pi (((oContMaps (f,X)) .: A),x) c= pi (A,(f . x)) :: according to XBOOLE_0:def_10 ::_thesis: pi (A,(f . x)) c= pi (((oContMaps (f,X)) .: A),x)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (((oContMaps (f,X)) .: A),x) or a in pi (A,(f . x)) )
assume  a in pi (((oContMaps (f,X)) .: A),x) ; ::_thesis: a in pi (A,(f . x))
then consider h being Function such that
A1: h in (oContMaps (f,X)) .: A and
A2: a = h . x by CARD_3:def_6;
consider g being set  such that
A3: g in the carrier of (oContMaps (Z,X)) and
A4: g in A and
A5: h = (oContMaps (f,X)) . g by A1, FUNCT_2:64;
reconsider g = g as continuous Function of Z,X by A3, Th2;
 h = g * f by A5, Def3;
then  a = g . (f . x) by A2, FUNCT_2:15;
hence  a in pi (A,(f . x)) by A4, CARD_3:def_6; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (A,(f . x)) or a in pi (((oContMaps (f,X)) .: A),x) )
assume  a in pi (A,(f . x)) ; ::_thesis: a in pi (((oContMaps (f,X)) .: A),x)
then consider g being Function such that
A6: g in A and
A7: a = g . (f . x) by CARD_3:def_6;
reconsider g = g as continuous Function of Z,X by A6, Th2;
 g * f = (oContMaps (f,X)) . g by Def3;
then A8: g * f in (oContMaps (f,X)) .: A by A6, FUNCT_2:35;
 a = (g * f) . x by A7, FUNCT_2:15;
hence  a in pi (((oContMaps (f,X)) .: A),x) by A8, CARD_3:def_6; ::_thesis: verum
end;

theorem Th15: :: WAYBEL26:15
for Y, Z being non empty TopSpace
for X being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving
proof
let Y, Z be non empty TopSpace; ::_thesis: for X being monotone-convergence T_0-TopSpace
for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving
let X be monotone-convergence T_0-TopSpace; ::_thesis: for f being continuous Function of Y,Z holds oContMaps (f,X) is directed-sups-preserving
let f be continuous Function of Y,Z; ::_thesis: oContMaps (f,X) is directed-sups-preserving
let A be Subset of (oContMaps (Z,X)); :: according to WAYBEL_0:def_37 ::_thesis: ( A is empty or not A is directed or oContMaps (f,X) preserves_sup_of A )
reconsider sA = sup A as continuous Function of Z,X by Th2;
set fX = oContMaps (f,X);
reconsider sfA = sup ((oContMaps (f,X)) .: A), XfsA = (oContMaps (f,X)) . (sup A) as Function of Y,(Omega X) by Th1;
reconsider YX = oContMaps (Y,X) as non empty full directed-sups-inheriting SubRelStr of (Omega X) |^ the carrier of Y by WAYBEL24:def_3, WAYBEL25:43;
assume  ( not A is empty & A is directed ) ; ::_thesis: oContMaps (f,X) preserves_sup_of A
then reconsider A9 = A as non empty directed Subset of (oContMaps (Z,X)) ;
reconsider fA9 = (oContMaps (f,X)) .: A9 as non empty directed Subset of (oContMaps (Y,X)) by Th10, YELLOW_2:15;
reconsider ZX = oContMaps (Z,X) as non empty full directed-sups-inheriting SubRelStr of (Omega X) |^ the carrier of Z by WAYBEL24:def_3, WAYBEL25:43;
reconsider B = A9 as non empty directed Subset of ZX ;
reconsider B9 = B as non empty directed Subset of ((Omega X) |^ the carrier of Z) by YELLOW_2:7;
reconsider fB = fA9 as non empty directed Subset of YX ;
reconsider fB9 = fB as non empty directed Subset of ((Omega X) |^ the carrier of Y) by YELLOW_2:7;
assume  ex_sup_of A, oContMaps (Z,X) ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (oContMaps (f,X)) .: A, oContMaps (Y,X) & "\/" (((oContMaps (f,X)) .: A),(oContMaps (Y,X))) = (oContMaps (f,X)) . ("\/" (A,(oContMaps (Z,X)))) )
set I1 = the carrier of Z;
set I2 = the carrier of Y;
set J1 = the carrier of Z --> (Omega X);
set J2 = the carrier of Y --> (Omega X);
 ex_sup_of fB9,(Omega X) |^ the carrier of Y by WAYBEL_0:75;
then A1: sup fB9 = sup ((oContMaps (f,X)) .: A) by WAYBEL_0:7;
 ( oContMaps (Y,X) is up-complete & fA9 is directed ) by Th7;
hence  ex_sup_of (oContMaps (f,X)) .: A, oContMaps (Y,X) by WAYBEL_0:75; ::_thesis: "\/" (((oContMaps (f,X)) .: A),(oContMaps (Y,X))) = (oContMaps (f,X)) . ("\/" (A,(oContMaps (Z,X))))
A2: (Omega X) |^ the carrier of Y = the carrier of Y -POS_prod ( the carrier of Y --> (Omega X)) by YELLOW_1:def_5;
then reconsider fB99 = fB9 as non empty directed Subset of ( the carrier of Y -POS_prod ( the carrier of Y --> (Omega X))) ;
now__::_thesis:_for_x_being_Element_of_Y_holds_ex_sup_of_pi_(fB99,x),(_the_carrier_of_Y_-->_(Omega_X))_._x
let x be Element of Y; ::_thesis: ex_sup_of pi (fB99,x),( the carrier of Y --> (Omega X)) . x
 ( ( the carrier of Y --> (Omega X)) . x = Omega X & pi (fB99,x) is directed ) by FUNCOP_1:7, YELLOW16:35;
hence  ex_sup_of pi (fB99,x),( the carrier of Y --> (Omega X)) . x by WAYBEL_0:75; ::_thesis: verum
end;
then A3: ex_sup_of fB99, the carrier of Y -POS_prod ( the carrier of Y --> (Omega X)) by YELLOW16:31;
A4: (Omega X) |^ the carrier of Z = the carrier of Z -POS_prod ( the carrier of Z --> (Omega X)) by YELLOW_1:def_5;
then reconsider B99 = B9 as non empty directed Subset of ( the carrier of Z -POS_prod ( the carrier of Z --> (Omega X))) ;
A5: ex_sup_of B9,(Omega X) |^ the carrier of Z by WAYBEL_0:75;
then A6: sup B9 = sup A by WAYBEL_0:7;
now__::_thesis:_for_x_being_Element_of_Y_holds_sfA_._x_=_XfsA_._x
let x be Element of Y; ::_thesis: sfA . x = XfsA . x
A7: ( ( the carrier of Z --> (Omega X)) . (f . x) = Omega X & ( the carrier of Y --> (Omega X)) . x = Omega X ) by FUNCOP_1:7;
A8: pi (fB99,x) = pi (B99,(f . x)) by Th14;
thus sfA . x = sup (pi (fB99,x)) by A1, A2, A3, YELLOW16:33
.= (sup B99) . (f . x) by A5, A4, A7, A8, YELLOW16:33
.= (sA * f) . x by A6, A4, FUNCT_2:15
.= XfsA . x by Def3 ; ::_thesis: verum
end;
hence  "\/" (((oContMaps (f,X)) .: A),(oContMaps (Y,X))) = (oContMaps (f,X)) . ("\/" (A,(oContMaps (Z,X)))) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: WAYBEL26:16
for X, Z being non empty TopSpace
for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
proof
let X, Z be non empty TopSpace; ::_thesis: for Y being non empty SubSpace of Z holds oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
let Y be non empty SubSpace of Z; ::_thesis: oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z)
set XY = oContMaps (X,Y);
set XZ = oContMaps (X,Z);
A1: Omega Y is full SubRelStr of Omega Z by WAYBEL25:17;
A2: [#] Y c= [#] Z by PRE_TOPC:def_4;
 oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)
proof
thus A3: the carrier of (oContMaps (X,Y)) c= the carrier of (oContMaps (X,Z)) :: according to YELLOW_0:def_13 ::_thesis: the InternalRel of (oContMaps (X,Y)) c= the InternalRel of (oContMaps (X,Z))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (oContMaps (X,Y)) or x in the carrier of (oContMaps (X,Z)) )
assume  x in the carrier of (oContMaps (X,Y)) ; ::_thesis: x in the carrier of (oContMaps (X,Z))
then reconsider f = x as continuous Function of X,Y by Th2;
 ( dom f = the carrier of X & rng f c= the carrier of Z ) by A2, FUNCT_2:def_1, XBOOLE_1:1;
then  x is continuous Function of X,Z by FUNCT_2:2, PRE_TOPC:26;
then  x is Element of (oContMaps (X,Z)) by Th2;
hence  x in the carrier of (oContMaps (X,Z)) ; ::_thesis: verum
end;
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Y)) or [x,y] in the InternalRel of (oContMaps (X,Z)) )
assume A4: [x,y] in the InternalRel of (oContMaps (X,Y)) ; ::_thesis: [x,y] in the InternalRel of (oContMaps (X,Z))
then A5: ( x in the carrier of (oContMaps (X,Y)) & y in the carrier of (oContMaps (X,Y)) ) by ZFMISC_1:87;
reconsider x = x, y = y as Element of (oContMaps (X,Y)) by A4, ZFMISC_1:87;
reconsider a = x, b = y as Element of (oContMaps (X,Z)) by A3, A5;
reconsider f = x, g = y as continuous Function of X,(Omega Y) by Th1;
reconsider f9 = a, g9 = b as continuous Function of X,(Omega Z) by Th1;
 x <= y by A4, ORDERS_2:def_5;
then  f <= g by Th3;
then  f9 <= g9 by A1, YELLOW16:2;
then  a <= b by Th3;
hence  [x,y] in the InternalRel of (oContMaps (X,Z)) by ORDERS_2:def_5; ::_thesis: verum
end;
then reconsider XY = oContMaps (X,Y) as non empty SubRelStr of oContMaps (X,Z) ;
A6: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY = the InternalRel of (oContMaps (X,Z)) /\ [: the carrier of XY, the carrier of XY:] by WELLORD1:def_6;
 the InternalRel of XY = the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY
proof
 the InternalRel of XY c= the InternalRel of (oContMaps (X,Z)) by YELLOW_0:def_13;
hence  the InternalRel of XY c= the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY by A6, XBOOLE_1:19; :: according to XBOOLE_0:def_10 ::_thesis: the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY c= the InternalRel of XY
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY or [x,y] in the InternalRel of XY )
assume A7: [x,y] in the InternalRel of (oContMaps (X,Z)) |_2 the carrier of XY ; ::_thesis: [x,y] in the InternalRel of XY
then A8: [x,y] in [: the carrier of XY, the carrier of XY:] by A6, XBOOLE_0:def_4;
then A9: ( x in the carrier of XY & y in the carrier of XY ) by ZFMISC_1:87;
reconsider x = x, y = y as Element of XY by A8, ZFMISC_1:87;
 the carrier of XY c= the carrier of (oContMaps (X,Z)) by YELLOW_0:def_13;
then reconsider a = x, b = y as Element of (oContMaps (X,Z)) by A9;
reconsider f9 = a, g9 = b as continuous Function of X,(Omega Z) by Th1;
reconsider f = x, g = y as continuous Function of X,(Omega Y) by Th1;
 [a,b] in the InternalRel of (oContMaps (X,Z)) by A6, A7, XBOOLE_0:def_4;
then  a <= b by ORDERS_2:def_5;
then  f9 <= g9 by Th3;
then  f <= g by A1, YELLOW16:3;
then  x <= y by Th3;
hence  [x,y] in the InternalRel of XY by ORDERS_2:def_5; ::_thesis: verum
end;
hence  oContMaps (X,Y) is full SubRelStr of oContMaps (X,Z) by YELLOW_0:def_14; ::_thesis: verum
end;

theorem Th17: :: WAYBEL26:17
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
proof
let Z be monotone-convergence T_0-TopSpace; ::_thesis: for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
let Y be non empty SubSpace of Z; ::_thesis: for f being continuous Function of Z,Y st f is being_a_retraction holds
Omega Y is directed-sups-inheriting SubRelStr of Omega Z
reconsider OZ = Omega Z as non empty up-complete Poset ;
reconsider OY = Omega Y as non empty full SubRelStr of Omega Z by WAYBEL25:17;
let f be continuous Function of Z,Y; ::_thesis: ( f is being_a_retraction implies Omega Y is directed-sups-inheriting SubRelStr of Omega Z )
A1: RelStr(# the carrier of OZ, the InternalRel of OZ #) = RelStr(# the carrier of (Omega Z), the InternalRel of (Omega Z) #) ;
 [#] Y c= [#] Z by PRE_TOPC:def_4;
then  ( dom f = the carrier of Z & rng f c= the carrier of Z ) by FUNCT_2:def_1, XBOOLE_1:1;
then A2: f is continuous Function of Z,Z by PRE_TOPC:26, RELSET_1:4;
 TopStruct(# the carrier of (Omega Z), the topology of (Omega Z) #) = TopStruct(# the carrier of Z, the topology of Z #) by WAYBEL25:def_2;
then reconsider f9 = f as continuous Function of (Omega Z),(Omega Z) by A2, YELLOW12:36;
reconsider g = f9 as Function of OZ,OZ ;
assume A3: f is being_a_retraction ; ::_thesis: Omega Y is directed-sups-inheriting SubRelStr of Omega Z
then  ( g is idempotent & g is directed-sups-preserving ) by YELLOW16:45;
then A4: Image g is directed-sups-inheriting by YELLOW16:6;
 ( TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) & rng g = the carrier of (subrelstr (rng g)) ) by WAYBEL25:def_2, YELLOW_0:def_15;
then  OY is directed-sups-inheriting by A3, A4, A1, WAYBEL21:22, YELLOW16:44;
hence  Omega Y is directed-sups-inheriting SubRelStr of Omega Z ; ::_thesis: verum
end;

Lm1:  for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
proof
let Z be monotone-convergence T_0-TopSpace; ::_thesis: for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
let Y be non empty SubSpace of Z; ::_thesis: for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence
let f be continuous Function of Z,Y; ::_thesis: ( f is being_a_retraction implies Y is monotone-convergence )
assume  f is being_a_retraction ; ::_thesis: Y is monotone-convergence
then  Y is_a_retract_of Z by BORSUK_1:def_17;
hence  Y is monotone-convergence by WAYBEL25:36, YELLOW16:56; ::_thesis: verum
end;

theorem Th18: :: WAYBEL26:18
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
proof
let X be non empty TopSpace; ::_thesis: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
let Z be monotone-convergence T_0-TopSpace; ::_thesis: for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
let Y be non empty SubSpace of Z; ::_thesis: for f being continuous Function of Z,Y st f is being_a_retraction holds
oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
set XY = oContMaps (X,Y);
set XZ = oContMaps (X,Z);
reconsider uXZ = oContMaps (X,Z) as non empty up-complete Poset by Th7;
let f be continuous Function of Z,Y; ::_thesis: ( f is being_a_retraction implies oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y) )
set F = oContMaps (X,f);
reconsider sXY = oContMaps (X,Y) as non empty full SubRelStr of uXZ by Th16;
assume A1: f is being_a_retraction ; ::_thesis: oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
then reconsider Y9 = Y as monotone-convergence T_0-TopSpace by Lm1;
 oContMaps (X,Y9) is up-complete by Th7;
hence  oContMaps (X,f) is directed-sups-preserving Function of (oContMaps (X,Z)),(oContMaps (X,Y)) by Th13; :: according to YELLOW16:def_1 ::_thesis: ( (oContMaps (X,f)) | the carrier of (oContMaps (X,Y)) = id (oContMaps (X,Y)) & oContMaps (X,Y) is SubRelStr of oContMaps (X,Z) )
A2: the carrier of sXY c= the carrier of uXZ by YELLOW_0:def_13;
A3: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_(oContMaps_(X,Y))_holds_
(id_(oContMaps_(X,Y)))_._x_=_((oContMaps_(X,f))_|_the_carrier_of_(oContMaps_(X,Y)))_._x
let x be set ; ::_thesis: ( x in the carrier of (oContMaps (X,Y)) implies (id (oContMaps (X,Y))) . x = ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x )
A4: dom f = the carrier of Z by FUNCT_2:def_1;
A5: ( rng f = the carrier of Y & f is idempotent ) by A1, YELLOW16:44, YELLOW16:45;
assume A6: x in the carrier of (oContMaps (X,Y)) ; ::_thesis: (id (oContMaps (X,Y))) . x = ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x
then reconsider a = x as Element of (oContMaps (X,Z)) by A2;
reconsider a = a as continuous Function of X,Z by Th2;
 x is Function of X,Y by A6, Th2;
then  rng a c= the carrier of Y by RELAT_1:def_19;
then  f * a = a by A5, A4, YELLOW16:4;
hence (id (oContMaps (X,Y))) . x = f * a by A6, FUNCT_1:18
.= (oContMaps (X,f)) . a by Def2
.= ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) . x by A6, FUNCT_1:49 ;
::_thesis: verum
end;
 (oContMaps (X,f)) | the carrier of (oContMaps (X,Y)) is Function of the carrier of (oContMaps (X,Y)), the carrier of (oContMaps (X,Y)) by A2, FUNCT_2:32;
then  ( dom (id (oContMaps (X,Y))) = the carrier of (oContMaps (X,Y)) & dom ((oContMaps (X,f)) | the carrier of (oContMaps (X,Y))) = the carrier of (oContMaps (X,Y)) ) by FUNCT_2:def_1;
hence  (oContMaps (X,f)) | the carrier of (oContMaps (X,Y)) = id (oContMaps (X,Y)) by A3, FUNCT_1:2; ::_thesis: oContMaps (X,Y) is SubRelStr of oContMaps (X,Z)
 Omega Y is full directed-sups-inheriting SubRelStr of Omega Z by A1, Th17, WAYBEL25:17;
then  ( oContMaps (X,Y9) is non empty full directed-sups-inheriting SubRelStr of (Omega Y) |^ the carrier of X & (Omega Y) |^ the carrier of X is full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X ) by WAYBEL24:def_3, WAYBEL25:43, YELLOW16:39, YELLOW16:42;
then  ( oContMaps (X,Z) is non empty full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X & oContMaps (X,Y) is full directed-sups-inheriting SubRelStr of (Omega Z) |^ the carrier of X ) by WAYBEL24:def_3, WAYBEL25:43, YELLOW16:26, YELLOW16:27;
hence  oContMaps (X,Y) is SubRelStr of oContMaps (X,Z) by Th16, YELLOW16:28; ::_thesis: verum
end;

theorem Th19: :: WAYBEL26:19
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)
proof
let X be non empty TopSpace; ::_thesis: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)
let Z be monotone-convergence T_0-TopSpace; ::_thesis: for Y being non empty SubSpace of Z st Y is_a_retract_of Z holds
oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)
let Y be non empty SubSpace of Z; ::_thesis: ( Y is_a_retract_of Z implies oContMaps (X,Y) is_a_retract_of oContMaps (X,Z) )
given f being continuous Function of Z,Y such that A1: f is being_a_retraction ; :: according to BORSUK_1:def_17 ::_thesis: oContMaps (X,Y) is_a_retract_of oContMaps (X,Z)
take  oContMaps (X,f) ; :: according to YELLOW16:def_3 ::_thesis: oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y)
thus  oContMaps (X,f) is_a_retraction_of oContMaps (X,Z), oContMaps (X,Y) by A1, Th18; ::_thesis: verum
end;

theorem Th20: :: WAYBEL26:20
for X, Y, Z being non empty TopSpace
for f being continuous Function of Y,Z st f is being_homeomorphism holds
oContMaps (X,f) is isomorphic
proof
let X, Y, Z be non empty TopSpace; ::_thesis: for f being continuous Function of Y,Z st f is being_homeomorphism holds
oContMaps (X,f) is isomorphic
let f be continuous Function of Y,Z; ::_thesis: ( f is being_homeomorphism implies oContMaps (X,f) is isomorphic )
set XY = oContMaps (X,Y);
set XZ = oContMaps (X,Z);
assume A1: f is being_homeomorphism ; ::_thesis: oContMaps (X,f) is isomorphic
then reconsider g = f " as continuous Function of Z,Y by TOPS_2:def_5;
set Xf = oContMaps (X,f);
set Xg = oContMaps (X,g);
A2: ( f is V7() & rng f = [#] Z ) by A1, TOPS_2:def_5;
now__::_thesis:_for_a_being_Element_of_(oContMaps_(X,Z))_holds_((oContMaps_(X,f))_*_(oContMaps_(X,g)))_._a_=_(id_(oContMaps_(X,Z)))_._a
let a be Element of (oContMaps (X,Z)); ::_thesis: ((oContMaps (X,f)) * (oContMaps (X,g))) . a = (id (oContMaps (X,Z))) . a
reconsider h = a as continuous Function of X,Z by Th2;
thus ((oContMaps (X,f)) * (oContMaps (X,g))) . a = (oContMaps (X,f)) . ((oContMaps (X,g)) . a) by FUNCT_2:15
.= (oContMaps (X,f)) . (g * h) by Def2
.= f * (g * h) by Def2
.= (f * g) * h by RELAT_1:36
.= (id the carrier of Z) * h by A2, TOPS_2:52
.= a by FUNCT_2:17
.= (id (oContMaps (X,Z))) . a by FUNCT_1:18 ; ::_thesis: verum
end;
then A3: (oContMaps (X,f)) * (oContMaps (X,g)) = id (oContMaps (X,Z)) by FUNCT_2:63;
A4: dom f = [#] Y by A1, TOPS_2:def_5;
now__::_thesis:_for_a_being_Element_of_(oContMaps_(X,Y))_holds_((oContMaps_(X,g))_*_(oContMaps_(X,f)))_._a_=_(id_(oContMaps_(X,Y)))_._a
let a be Element of (oContMaps (X,Y)); ::_thesis: ((oContMaps (X,g)) * (oContMaps (X,f))) . a = (id (oContMaps (X,Y))) . a
reconsider h = a as continuous Function of X,Y by Th2;
thus ((oContMaps (X,g)) * (oContMaps (X,f))) . a = (oContMaps (X,g)) . ((oContMaps (X,f)) . a) by FUNCT_2:15
.= (oContMaps (X,g)) . (f * h) by Def2
.= g * (f * h) by Def2
.= (g * f) * h by RELAT_1:36
.= (id the carrier of Y) * h by A2, A4, TOPS_2:52
.= a by FUNCT_2:17
.= (id (oContMaps (X,Y))) . a by FUNCT_1:18 ; ::_thesis: verum
end;
then A5: (oContMaps (X,g)) * (oContMaps (X,f)) = id (oContMaps (X,Y)) by FUNCT_2:63;
 ( oContMaps (X,f) is monotone & oContMaps (X,g) is monotone ) by Th8;
hence  oContMaps (X,f) is isomorphic by A5, A3, YELLOW16:15; ::_thesis: verum
end;

theorem Th21: :: WAYBEL26:21
for X, Y, Z being non empty TopSpace st Y,Z are_homeomorphic holds
oContMaps (X,Y), oContMaps (X,Z) are_isomorphic
proof
let X, Y, Z be non empty TopSpace; ::_thesis: ( Y,Z are_homeomorphic implies oContMaps (X,Y), oContMaps (X,Z) are_isomorphic )
given f being Function of Y,Z such that A1: f is being_homeomorphism ; :: according to T_0TOPSP:def_1 ::_thesis: oContMaps (X,Y), oContMaps (X,Z) are_isomorphic
reconsider f = f as continuous Function of Y,Z by A1, TOPS_2:def_5;
take  oContMaps (X,f) ; :: according to WAYBEL_1:def_8 ::_thesis: oContMaps (X,f) is isomorphic
thus  oContMaps (X,f) is isomorphic by A1, Th20; ::_thesis: verum
end;

theorem Th22: :: WAYBEL26:22
for X being non empty TopSpace
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
proof
let X be non empty TopSpace; ::_thesis: for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
let Z be monotone-convergence T_0-TopSpace; ::_thesis: for Y being non empty SubSpace of Z st Y is_a_retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
let Y be non empty SubSpace of Z; ::_thesis: ( Y is_a_retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous implies ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
assume  Y is_a_retract_of Z ; ::_thesis: ( not oContMaps (X,Z) is complete or not oContMaps (X,Z) is continuous or ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
then A1: oContMaps (X,Y) is_a_retract_of oContMaps (X,Z) by Th19;
assume  ( oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous ) ; ::_thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
hence  ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A1, YELLOW16:21, YELLOW16:22; ::_thesis: verum
end;

theorem Th23: :: WAYBEL26:23
for X being non empty TopSpace
for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
proof
let X be non empty TopSpace; ::_thesis: for Y, Z being monotone-convergence T_0-TopSpace st Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
let Y, Z be monotone-convergence T_0-TopSpace; ::_thesis: ( Y is_Retract_of Z & oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous implies ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
assume  Y is_Retract_of Z ; ::_thesis: ( not oContMaps (X,Z) is complete or not oContMaps (X,Z) is continuous or ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
then consider S being non empty SubSpace of Z such that
A1: S is_a_retract_of Z and
A2: S,Y are_homeomorphic by YELLOW16:57;
assume  ( oContMaps (X,Z) is complete & oContMaps (X,Z) is continuous ) ; ::_thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
then A3: ( oContMaps (X,S) is complete & oContMaps (X,S) is continuous ) by A1, Th22;
 oContMaps (X,S), oContMaps (X,Y) are_isomorphic by A2, Th21;
hence  ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A3, WAYBEL15:9, WAYBEL20:18; ::_thesis: verum
end;

theorem Th24: :: WAYBEL26:24
for Y being non trivial T_0-TopSpace st not Y is T_1 holds
Sierpinski_Space is_Retract_of Y
proof
let Y be non trivial T_0-TopSpace; ::_thesis: ( not Y is T_1 implies Sierpinski_Space is_Retract_of Y )
given p, q being Point of Y such that A1: p <> q and
A2: for W, V being Subset of Y st W is open & V is open & p in W & not q in W & q in V holds
p in V ; :: according to URYSOHN1:def_7 ::_thesis: Sierpinski_Space is_Retract_of Y
 ( ex V being Subset of Y st
( V is open & p in V & not q in V ) or ex W being Subset of Y st
( W is open & not p in W & q in W ) ) by A1, TSP_1:def_3;
then consider V being Subset of Y such that
A3: V is open and
A4: ( ( p in V & not q in V ) or ( not p in V & q in V ) ) ;
A5: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def_2;
then consider x, y being Element of (Omega Y) such that
A6: ( ( p in V & not q in V & x = q & y = p ) or ( not p in V & q in V & x = p & y = q ) ) by A4;
now__::_thesis:_for_W_being_open_Subset_of_(Omega_Y)_st_x_in_W_holds_
y_in_W
let W be open Subset of (Omega Y); ::_thesis: ( x in W implies y in W )
 W is open Subset of Y by A5, TOPS_3:76;
hence  ( x in W implies y in W ) by A2, A3, A6; ::_thesis: verum
end;
then  (0,1) --> (x,y) is continuous Function of Sierpinski_Space,(Omega Y) by YELLOW16:47;
then reconsider i = (0,1) --> (x,y) as continuous Function of Sierpinski_Space,Y by A5, YELLOW12:36;
reconsider V = V as open Subset of (Omega Y) by A3, A5, TOPS_3:76;
reconsider c = chi (V, the carrier of Y) as continuous Function of Y,Sierpinski_Space by A3, YELLOW16:46;
 c * i = id Sierpinski_Space by A5, A6, YELLOW16:48;
hence  Sierpinski_Space is_Retract_of Y by WAYBEL25:def_1; ::_thesis: verum
end;

theorem Th25: :: WAYBEL26:25
for X being non empty TopSpace
for Y being non trivial T_0-TopSpace st oContMaps (X,Y) is with_suprema holds
not Y is T_1
proof
let X be non empty TopSpace; ::_thesis: for Y being non trivial T_0-TopSpace st oContMaps (X,Y) is with_suprema holds
not Y is T_1
let Y be non trivial T_0-TopSpace; ::_thesis: ( oContMaps (X,Y) is with_suprema implies not Y is T_1 )
consider a, b being Element of Y such that
A1: a <> b by STRUCT_0:def_10;
set i = the Element of X;
reconsider f = X --> a, g = X --> b as continuous Function of X,Y ;
assume  oContMaps (X,Y) is with_suprema ; ::_thesis: not Y is T_1
then reconsider XY = oContMaps (X,Y) as sup-Semilattice ;
reconsider ef = f, eg = g as Element of XY by Th2;
reconsider h = ef "\/" eg, f = ef, g = eg as continuous Function of X,(Omega Y) by Th1;
A2: ( f . the Element of X = a & g . the Element of X = b ) by FUNCOP_1:7;
now__::_thesis:_ex_x,_y_being_Element_of_(Omega_Y)_st_
(_x_<=_y_&_x_<>_y_)
 eg <= ef "\/" eg by YELLOW_0:22;
then  g <= h by Th3;
then A3: ex x, y being Element of (Omega Y) st
( x = g . the Element of X & y = h . the Element of X & x <= y ) by YELLOW_2:def_1;
 ef <= ef "\/" eg by YELLOW_0:22;
then  f <= h by Th3;
then A4: ex x, y being Element of (Omega Y) st
( x = f . the Element of X & y = h . the Element of X & x <= y ) by YELLOW_2:def_1;
assume A5: for x, y being Element of (Omega Y) holds
( not x <= y or not x <> y ) ; ::_thesis: contradiction
then  ( not f . the Element of X <= h . the Element of X or not f . the Element of X <> h . the Element of X ) ;
hence  contradiction by A1, A2, A5, A4, A3; ::_thesis: verum
end;
then consider x, y being Element of (Omega Y) such that
A6: x <= y and
A7: x <> y ;
A8: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def_2;
then reconsider p = x, q = y as Element of Y ;
take  p ; :: according to URYSOHN1:def_7 ::_thesis: ex b1 being Element of the carrier of Y st
( not p = b1 & ( for b2, b3 being Element of bool the carrier of Y holds
( not b2 is open or not b3 is open or not p in b2 or b1 in b2 or not b1 in b3 or p in b3 ) ) )
take  q ; ::_thesis: ( not p = q & ( for b1, b2 being Element of bool the carrier of Y holds
( not b1 is open or not b2 is open or not p in b1 or q in b1 or not q in b2 or p in b2 ) ) )
thus  p <> q by A7; ::_thesis: for b1, b2 being Element of bool the carrier of Y holds
( not b1 is open or not b2 is open or not p in b1 or q in b1 or not q in b2 or p in b2 )
let W, V be Subset of Y; ::_thesis: ( not W is open or not V is open or not p in W or q in W or not q in V or p in V )
assume  W is open ; ::_thesis: ( not V is open or not p in W or q in W or not q in V or p in V )
then reconsider W = W as open Subset of (Omega Y) by A8, TOPS_3:76;
 W is upper ;
hence  ( not V is open or not p in W or q in W or not q in V or p in V ) by A6, WAYBEL_0:def_20; ::_thesis: verum
end;

registration
cluster Sierpinski_Space  ->  non trivial monotone-convergence ;
coherence
 ( not Sierpinski_Space is trivial & Sierpinski_Space is monotone-convergence )
proof
A1: 1 in {0,1} by TARSKI:def_2;
 ( the carrier of Sierpinski_Space = {0,1} & 0 in {0,1} ) by TARSKI:def_2, WAYBEL18:def_9;
hence  ( not Sierpinski_Space is trivial & Sierpinski_Space is monotone-convergence ) by A1, STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
cluster non empty non trivial TopSpace-like T_0 injective monotone-convergence for TopStruct ;
existence
 ex b1 being T_0-TopSpace st
( b1 is injective & b1 is monotone-convergence & not b1 is trivial )
proof
take  Sierpinski_Space ; ::_thesis: ( Sierpinski_Space is injective & Sierpinski_Space is monotone-convergence & not Sierpinski_Space is trivial )
thus  ( Sierpinski_Space is injective & Sierpinski_Space is monotone-convergence & not Sierpinski_Space is trivial ) ; ::_thesis: verum
end;
end;

theorem Th26: :: WAYBEL26:26
for X being non empty TopSpace
for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds
InclPoset the topology of X is continuous
proof
let X be non empty TopSpace; ::_thesis: for Y being non trivial monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds
InclPoset the topology of X is continuous
let Y be non trivial monotone-convergence T_0-TopSpace; ::_thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous implies InclPoset the topology of X is continuous )
assume A1: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) ; ::_thesis: InclPoset the topology of X is continuous
then  Sierpinski_Space is_Retract_of Y by Th24, Th25;
then A2: ( oContMaps (X,Sierpinski_Space) is complete & oContMaps (X,Sierpinski_Space) is continuous ) by A1, Th23;
 InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by Th6;
hence  InclPoset the topology of X is continuous by A2, WAYBEL15:9, WAYBEL_1:6; ::_thesis: verum
end;

theorem Th27: :: WAYBEL26:27
for X being non empty TopSpace
for x being Point of X
for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X
for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )
let x be Point of X; ::_thesis: for Y being monotone-convergence T_0-TopSpace ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )
let Y be monotone-convergence T_0-TopSpace; ::_thesis: ex F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) st
( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )
set XY = oContMaps (X,Y);
reconsider f = X --> x as continuous Function of X,X ;
set F = oContMaps (f,Y);
 dom f = the carrier of X by FUNCT_2:def_1;
then f * f = the carrier of X --> (f . x) by FUNCOP_1:17
.= f by FUNCOP_1:7 ;
then  f is idempotent by QUANTAL1:def_9;
then  oContMaps (f,Y) is idempotent directed-sups-preserving Function of (oContMaps (X,Y)),(oContMaps (X,Y)) by Th11, Th15;
then reconsider F = oContMaps (f,Y) as directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) by WAYBEL_1:def_13;
take  F ; ::_thesis: ( ( for f being continuous Function of X,Y holds F . f = X --> (f . x) ) & ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) )
hereby  ::_thesis: ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) )
let h be continuous Function of X,Y; ::_thesis: F . h = X --> (h . x)
A1: the carrier of X = dom h by FUNCT_2:def_1;
thus F . h = h * ( the carrier of X --> x) by Def3
.= X --> (h . x) by A1, FUNCOP_1:17 ; ::_thesis: verum
end;
thus  ex h being continuous Function of X,X st
( h = X --> x & F = oContMaps (h,Y) ) ; ::_thesis: verum
end;

theorem Th28: :: WAYBEL26:28
for X being non empty TopSpace
for Y being monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds
( Omega Y is complete & Omega Y is continuous )
proof
let X be non empty TopSpace; ::_thesis: for Y being monotone-convergence T_0-TopSpace st oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous holds
( Omega Y is complete & Omega Y is continuous )
let Y be monotone-convergence T_0-TopSpace; ::_thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous implies ( Omega Y is complete & Omega Y is continuous ) )
assume A1: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) ; ::_thesis: ( Omega Y is complete & Omega Y is continuous )
set b = the Element of X;
A2: TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) = TopStruct(# the carrier of Y, the topology of Y #) by WAYBEL25:def_2;
consider F being directed-sups-preserving projection Function of (oContMaps (X,Y)),(oContMaps (X,Y)) such that
A3: for f being continuous Function of X,Y holds F . f = X --> (f . the Element of X) and
 ex h being continuous Function of X,X st
( h = X --> the Element of X & F = oContMaps (h,Y) ) by Th27;
 oContMaps (X,Y) is full SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then reconsider imF = Image F as non empty full SubRelStr of (Omega Y) |^ the carrier of X by YELLOW16:26;
A4: the carrier of imF = rng F by YELLOW_0:def_15;
A5: dom F = the carrier of (oContMaps (X,Y)) by FUNCT_2:52;
now__::_thesis:_for_a_being_set_holds_
(_(_a_is_Element_of_imF_implies_ex_x_being_Element_of_(Omega_Y)_st_a_=_the_carrier_of_X_-->_x_)_&_(_ex_x_being_Element_of_(Omega_Y)_st_a_=_the_carrier_of_X_-->_x_implies_a_is_Element_of_imF_)_)
let a be set ; ::_thesis: ( ( a is Element of imF implies ex x being Element of (Omega Y) st a = the carrier of X --> x ) & ( ex x being Element of (Omega Y) st a = the carrier of X --> x implies a is Element of imF ) )
hereby  ::_thesis: ( ex x being Element of (Omega Y) st a = the carrier of X --> x implies a is Element of imF )
assume  a is Element of imF ; ::_thesis: ex x being Element of (Omega Y) st a = the carrier of X --> x
then consider h being set  such that
A6: h in dom F and
A7: a = F . h by A4, FUNCT_1:def_3;
reconsider h = h as continuous Function of X,Y by A6, Th2;
reconsider x = h . the Element of X as Element of (Omega Y) by A2;
a = X --> (h . the Element of X) by A3, A7
.= the carrier of X --> x ;
hence  ex x being Element of (Omega Y) st a = the carrier of X --> x ; ::_thesis: verum
end;
given x being Element of (Omega Y) such that A8: a = the carrier of X --> x ; ::_thesis: a is Element of imF
 a = X --> x by A8;
then A9: a is Element of (oContMaps (X,Y)) by Th1;
then reconsider h = a as continuous Function of X,Y by Th2;
A10: X --> (h . the Element of X) = the carrier of X --> (h . the Element of X) ;
 h . the Element of X = x by A8, FUNCOP_1:7;
then  F . a = X --> x by A3, A10;
hence  a is Element of imF by A4, A5, A8, A9, FUNCT_1:def_3; ::_thesis: verum
end;
then  Omega Y,imF are_isomorphic by YELLOW16:50;
then A11: imF, Omega Y are_isomorphic by WAYBEL_1:6;
 Image F is complete continuous LATTICE by A1, WAYBEL15:15, YELLOW_2:35;
hence  ( Omega Y is complete & Omega Y is continuous ) by A11, WAYBEL15:9, WAYBEL20:18; ::_thesis: verum
end;

theorem Th29: :: WAYBEL26:29
for X being non empty 1-sorted
for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj (J,i)) * f
proof
let X be non empty 1-sorted ; ::_thesis: for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj (J,i)) * f
let I be non empty set ; ::_thesis: for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj (J,i)) * f
let J be non-Empty TopStruct-yielding ManySortedSet of I; ::_thesis: for f being Function of X,(I -TOP_prod J)
for i being Element of I holds (commute f) . i = (proj (J,i)) * f
let f be Function of X,(I -TOP_prod J); ::_thesis: for i being Element of I holds (commute f) . i = (proj (J,i)) * f
A1: the carrier of (I -TOP_prod J) = product (Carrier J) by WAYBEL18:def_3;
let i be Element of I; ::_thesis: (commute f) . i = (proj (J,i)) * f
A2: dom (Carrier J) = I by PARTFUN1:def_2;
A3: rng f c= Funcs (I,(Union (Carrier J)))
proof
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng f or g in Funcs (I,(Union (Carrier J))) )
assume  g in rng f ; ::_thesis: g in Funcs (I,(Union (Carrier J)))
then consider h being Function such that
A4: g = h and
A5: dom h = I and
A6: for x being set st x in I holds
h . x in (Carrier J) . x by A1, A2, CARD_3:def_5;
 rng h c= Union (Carrier J)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h or y in Union (Carrier J) )
A7: dom (Carrier J) = I by PARTFUN1:def_2;
assume  y in rng h ; ::_thesis: y in Union (Carrier J)
then consider x being set  such that
A8: x in dom h and
A9: y = h . x by FUNCT_1:def_3;
 h . x in (Carrier J) . x by A5, A6, A8;
hence  y in Union (Carrier J) by A5, A8, A9, A7, CARD_5:2; ::_thesis: verum
end;
hence  g in Funcs (I,(Union (Carrier J))) by A4, A5, FUNCT_2:def_2; ::_thesis: verum
end;
 dom f = the carrier of X by FUNCT_2:def_1;
then A10: f in Funcs ( the carrier of X,(Funcs (I,(Union (Carrier J))))) by A3, FUNCT_2:def_2;
then  commute f in Funcs (I,(Funcs ( the carrier of X,(Union (Carrier J))))) by FUNCT_6:55;
then A11: ex g being Function st
( commute f = g & dom g = I & rng g c= Funcs ( the carrier of X,(Union (Carrier J))) ) by FUNCT_2:def_2;
then  (commute f) . i in rng (commute f) by FUNCT_1:def_3;
then consider g being Function such that
A12: (commute f) . i = g and
A13: dom g = the carrier of X and
 rng g c= Union (Carrier J) by A11, FUNCT_2:def_2;
A14: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_X_holds_
g_._x_=_((proj_(J,i))_*_f)_._x
let x be set ; ::_thesis: ( x in the carrier of X implies g . x = ((proj (J,i)) * f) . x )
A15: dom (proj ((Carrier J),i)) = product (Carrier J) by CARD_3:def_16;
assume  x in the carrier of X ; ::_thesis: g . x = ((proj (J,i)) * f) . x
then reconsider a = x as Element of X ;
consider h being Function such that
A16: f . a = h and
 dom h = I and
 for x being set st x in I holds
h . x in (Carrier J) . x by A1, A2, CARD_3:def_5;
((proj (J,i)) * f) . a = (proj (J,i)) . (f . a) by FUNCT_2:15
.= (proj ((Carrier J),i)) . (f . a) by WAYBEL18:def_4
.= h . i by A1, A16, A15, CARD_3:def_16 ;
hence  g . x = ((proj (J,i)) * f) . x by A10, A12, A16, FUNCT_6:56; ::_thesis: verum
end;
 dom ((proj (J,i)) * f) = the carrier of X by FUNCT_2:def_1;
hence  (commute f) . i = (proj (J,i)) * f by A12, A13, A14, FUNCT_1:2; ::_thesis: verum
end;

theorem Th30: :: WAYBEL26:30
for S being 1-sorted
for M being set holds Carrier (M --> S) = M --> the carrier of S
proof
let S be 1-sorted ; ::_thesis: for M being set holds Carrier (M --> S) = M --> the carrier of S
let M be set ; ::_thesis: Carrier (M --> S) = M --> the carrier of S
now__::_thesis:_for_i_being_set_st_i_in_M_holds_
(Carrier_(M_-->_S))_._i_=_(M_-->_the_carrier_of_S)_._i
let i be set ; ::_thesis: ( i in M implies (Carrier (M --> S)) . i = (M --> the carrier of S) . i )
assume A1: i in M ; ::_thesis: (Carrier (M --> S)) . i = (M --> the carrier of S) . i
then  ( (M --> S) . i = S & ex R being 1-sorted st
( R = (M --> S) . i & (Carrier (M --> S)) . i = the carrier of R ) ) by FUNCOP_1:7, PRALG_1:def_13;
hence  (Carrier (M --> S)) . i = (M --> the carrier of S) . i by A1, FUNCOP_1:7; ::_thesis: verum
end;
hence  Carrier (M --> S) = M --> the carrier of S by PBOOLE:3; ::_thesis: verum
end;

theorem Th31: :: WAYBEL26:31
for X, Y being non empty TopSpace
for M being non empty set
for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M, the carrier of (oContMaps (X,Y))
proof
let X, Y be non empty TopSpace; ::_thesis: for M being non empty set
for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M, the carrier of (oContMaps (X,Y))
let M be non empty set ; ::_thesis: for f being continuous Function of X,(M -TOP_prod (M --> Y)) holds commute f is Function of M, the carrier of (oContMaps (X,Y))
let f be continuous Function of X,(M -TOP_prod (M --> Y)); ::_thesis: commute f is Function of M, the carrier of (oContMaps (X,Y))
A1: rng f c= Funcs (M, the carrier of Y)
proof
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng f or g in Funcs (M, the carrier of Y) )
assume A2: g in rng f ; ::_thesis: g in Funcs (M, the carrier of Y)
A3: dom (M --> the carrier of Y) = M by FUNCOP_1:13;
the carrier of (M -TOP_prod (M --> Y)) = product (Carrier (M --> Y)) by WAYBEL18:def_3
.= product (M --> the carrier of Y) by Th30 ;
then consider h being Function such that
A4: g = h and
A5: dom h = M and
A6: for x being set st x in M holds
h . x in (M --> the carrier of Y) . x by A2, A3, CARD_3:def_5;
 rng h c= the carrier of Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng h or y in the carrier of Y )
assume  y in rng h ; ::_thesis: y in the carrier of Y
then consider x being set  such that
A7: x in dom h and
A8: y = h . x by FUNCT_1:def_3;
 (M --> the carrier of Y) . x = the carrier of Y by A5, A7, FUNCOP_1:7;
hence  y in the carrier of Y by A5, A6, A7, A8; ::_thesis: verum
end;
hence  g in Funcs (M, the carrier of Y) by A4, A5, FUNCT_2:def_2; ::_thesis: verum
end;
 dom f = the carrier of X by FUNCT_2:def_1;
then  f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by A1, FUNCT_2:def_2;
then A9: commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:55;
A10: rng (commute f) c= the carrier of (oContMaps (X,Y))
proof
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng (commute f) or g in the carrier of (oContMaps (X,Y)) )
assume  g in rng (commute f) ; ::_thesis: g in the carrier of (oContMaps (X,Y))
then consider i being set  such that
A11: i in dom (commute f) and
A12: g = (commute f) . i by FUNCT_1:def_3;
 ex h being Function st
( commute f = h & dom h = M & rng h c= Funcs ( the carrier of X, the carrier of Y) ) by A9, FUNCT_2:def_2;
then reconsider i = i as Element of M by A11;
A13: (M --> Y) . i = Y by FUNCOP_1:7;
 g = (proj ((M --> Y),i)) * f by A12, Th29;
then  g is continuous Function of X,Y by A13, WAYBEL18:6;
then  g is Element of (oContMaps (X,Y)) by Th2;
hence  g in the carrier of (oContMaps (X,Y)) ; ::_thesis: verum
end;
 ex g being Function st
( commute f = g & dom g = M & rng g c= Funcs ( the carrier of X, the carrier of Y) ) by A9, FUNCT_2:def_2;
hence  commute f is Function of M, the carrier of (oContMaps (X,Y)) by A10, FUNCT_2:2; ::_thesis: verum
end;

theorem Th32: :: WAYBEL26:32
for X, Y being non empty TopSpace holds the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y)
proof
let X, Y be non empty TopSpace; ::_thesis: the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y)
 oContMaps (X,Y) is SubRelStr of (Omega Y) |^ the carrier of X by WAYBEL24:def_3;
then A1: the carrier of (oContMaps (X,Y)) c= the carrier of ((Omega Y) |^ the carrier of X) by YELLOW_0:def_13;
 TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of (Omega Y), the topology of (Omega Y) #) by WAYBEL25:def_2;
hence  the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y) by A1, YELLOW_1:28; ::_thesis: verum
end;

theorem Th33: :: WAYBEL26:33
for X, Y being non empty TopSpace
for M being non empty set
for f being Function of M, the carrier of (oContMaps (X,Y)) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
proof
let X, Y be non empty TopSpace; ::_thesis: for M being non empty set
for f being Function of M, the carrier of (oContMaps (X,Y)) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
let M be non empty set ; ::_thesis: for f being Function of M, the carrier of (oContMaps (X,Y)) holds commute f is continuous Function of X,(M -TOP_prod (M --> Y))
let f be Function of M, the carrier of (oContMaps (X,Y)); ::_thesis: commute f is continuous Function of X,(M -TOP_prod (M --> Y))
reconsider B = product_prebasis (M --> Y) as prebasis of (M -TOP_prod (M --> Y)) by WAYBEL18:def_3;
A1: Carrier (M --> Y) = M --> the carrier of Y by Th30;
 the carrier of (oContMaps (X,Y)) c= Funcs ( the carrier of X, the carrier of Y) by Th32;
then  ( dom f = M & rng f c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def_1, XBOOLE_1:1;
then A2: f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_2:def_2;
then  commute f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by FUNCT_6:55;
then A3: ex g being Function st
( commute f = g & dom g = the carrier of X & rng g c= Funcs (M, the carrier of Y) ) by FUNCT_2:def_2;
 the carrier of (M -TOP_prod (M --> Y)) = product (Carrier (M --> Y)) by WAYBEL18:def_3;
then  the carrier of (M -TOP_prod (M --> Y)) = Funcs (M, the carrier of Y) by A1, CARD_3:11;
then reconsider g = commute f as Function of X,(M -TOP_prod (M --> Y)) by A3, FUNCT_2:2;
now__::_thesis:_for_P_being_Subset_of_(M_-TOP_prod_(M_-->_Y))_st_P_in_B_holds_
g_"_P_is_open
let P be Subset of (M -TOP_prod (M --> Y)); ::_thesis: ( P in B implies g " P is open )
assume  P in B ; ::_thesis: g " P is open
then consider i being set , T being TopStruct , V being Subset of T such that
A4: i in M and
A5: V is open and
A6: T = (M --> Y) . i and
A7: P = product ((Carrier (M --> Y)) +* (i,V)) by WAYBEL18:def_2;
reconsider i = i as Element of M by A4;
set FP = (Carrier (M --> Y)) +* (i,V);
A8: dom ((Carrier (M --> Y)) +* (i,V)) = dom (Carrier (M --> Y)) by FUNCT_7:30;
reconsider fi = f . i as continuous Function of X,Y by Th2;
A9: dom (Carrier (M --> Y)) = M by A1, FUNCOP_1:13;
then A10: ((Carrier (M --> Y)) +* (i,V)) . i = V by FUNCT_7:31;
A11: T = Y by A4, A6, FUNCOP_1:7;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_g_"_P_implies_ex_Q_being_Subset_of_X_st_
(_Q_is_open_&_Q_c=_g_"_P_&_x_in_Q_)_)_&_(_ex_Q_being_Subset_of_X_st_
(_Q_is_open_&_Q_c=_g_"_P_&_x_in_Q_)_implies_x_in_g_"_P_)_)
let x be set ; ::_thesis: ( ( x in g " P implies ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) implies x in g " P ) )
hereby  ::_thesis: ( ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) implies x in g " P )
reconsider Q = fi " V as Subset of X ;
assume A12: x in g " P ; ::_thesis: ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q )
then  g . x in P by FUNCT_2:38;
then consider gx being Function such that
A13: g . x = gx and
 dom gx = dom ((Carrier (M --> Y)) +* (i,V)) and
A14: for z being set st z in dom ((Carrier (M --> Y)) +* (i,V)) holds
gx . z in ((Carrier (M --> Y)) +* (i,V)) . z by A7, CARD_3:def_5;
A15: gx . i = fi . x by A2, A12, A13, FUNCT_6:56;
take Q = Q; ::_thesis: ( Q is open & Q c= g " P & x in Q )
 [#] Y <> {} ;
hence  Q is open by A5, A11, TOPS_2:43; ::_thesis: ( Q c= g " P & x in Q )
thus  Q c= g " P ::_thesis: x in Q
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Q or a in g " P )
assume A16: a in Q ; ::_thesis: a in g " P
then  g . a in rng g by A3, FUNCT_1:def_3;
then consider ga being Function such that
A17: g . a = ga and
A18: dom ga = M and
A19: rng ga c= the carrier of Y by A3, FUNCT_2:def_2;
A20: fi . a in V by A16, FUNCT_2:38;
now__::_thesis:_for_z_being_set_st_z_in_M_holds_
ga_._z_in_((Carrier_(M_-->_Y))_+*_(i,V))_._z
let z be set ; ::_thesis: ( z in M implies ga . z in ((Carrier (M --> Y)) +* (i,V)) . z )
assume A21: z in M ; ::_thesis: ga . z in ((Carrier (M --> Y)) +* (i,V)) . z
then  ( ( z <> i & (M --> the carrier of Y) . z = the carrier of Y ) or z = i ) by FUNCOP_1:7;
then  ( ( z <> i & ga . z in rng ga & ((Carrier (M --> Y)) +* (i,V)) . z = the carrier of Y ) or z = i ) by A1, A18, A21, FUNCT_1:def_3, FUNCT_7:32;
hence  ga . z in ((Carrier (M --> Y)) +* (i,V)) . z by A2, A10, A16, A20, A17, A19, FUNCT_6:56; ::_thesis: verum
end;
then  ga in P by A7, A8, A9, A18, CARD_3:9;
hence  a in g " P by A16, A17, FUNCT_2:38; ::_thesis: verum
end;
 gx . i in V by A8, A9, A10, A14;
hence  x in Q by A12, A15, FUNCT_2:38; ::_thesis: verum
end;
thus  ( ex Q being Subset of X st
( Q is open & Q c= g " P & x in Q ) implies x in g " P ) ; ::_thesis: verum
end;
hence  g " P is open by TOPS_1:25; ::_thesis: verum
end;
hence  commute f is continuous Function of X,(M -TOP_prod (M --> Y)) by YELLOW_9:36; ::_thesis: verum
end;

theorem Th34: :: WAYBEL26:34
for X being non empty TopSpace
for M being non empty set ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st
( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
proof
let X be non empty TopSpace; ::_thesis: for M being non empty set ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st
( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
let M be non empty set ; ::_thesis: ex F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) st
( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
set S = Sierpinski_Space ;
set S9M = M -TOP_prod (M --> Sierpinski_Space);
set XxxS9M = oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)));
set XxS = oContMaps (X,Sierpinski_Space);
set XxS9xM = M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)));
deffunc H1( Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) ->  set = commute $1;
consider F being ManySortedSet of the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) such that
A1: for f being Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) holds F . f = H1(f) from PBOOLE:sch_5();
A2: dom F = the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by PARTFUN1:def_2;
 rng F c= the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))
proof
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng F or g in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) )
assume  g in rng F ; ::_thesis: g in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))
then consider f being set  such that
A3: f in dom F and
A4: g = F . f by FUNCT_1:def_3;
reconsider f = f as continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) by A3, Th2;
 g = commute f by A1, A3, A4;
then reconsider g = g as Function of M, the carrier of (oContMaps (X,Sierpinski_Space)) by Th31;
 ( dom g = M & rng g c= the carrier of (oContMaps (X,Sierpinski_Space)) ) by FUNCT_2:def_1;
then  g in Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) by FUNCT_2:def_2;
then  g in the carrier of ((oContMaps (X,Sierpinski_Space)) |^ M) by YELLOW_1:28;
hence  g in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by YELLOW_1:def_5; ::_thesis: verum
end;
then reconsider F = F as Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by A2, FUNCT_2:2;
deffunc H2( Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) ->  set = commute $1;
consider G being ManySortedSet of the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) such that
A5: for f being Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) holds G . f = H2(f) from PBOOLE:sch_5();
A6: dom G = the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by PARTFUN1:def_2;
A7: rng G c= the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))
proof
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng G or g in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) )
assume  g in rng G ; ::_thesis: g in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))
then consider f being set  such that
A8: f in dom G and
A9: g = G . f by FUNCT_1:def_3;
 f in the carrier of ((oContMaps (X,Sierpinski_Space)) |^ M) by A6, A8, YELLOW_1:def_5;
then  f in Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) by YELLOW_1:28;
then consider f9 being Function such that
A10: f = f9 and
A11: ( dom f9 = M & rng f9 c= the carrier of (oContMaps (X,Sierpinski_Space)) ) by FUNCT_2:def_2;
A12: f9 is Function of M, the carrier of (oContMaps (X,Sierpinski_Space)) by A11, FUNCT_2:2;
 g = commute f9 by A5, A8, A9, A10;
then  g is continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) by A12, Th33;
then  g is Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by Th2;
hence  g in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) ; ::_thesis: verum
end;
take  F ; ::_thesis: ( F is isomorphic & ( for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f ) )
A13: the carrier of (M -TOP_prod (M --> Sierpinski_Space)) = product (Carrier (M --> Sierpinski_Space)) by WAYBEL18:def_3
.= product (M --> the carrier of Sierpinski_Space) by Th30
.= Funcs (M, the carrier of Sierpinski_Space) by CARD_3:11 ;
reconsider G = G as Function of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))),(oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by A6, A7, FUNCT_2:2;
A14: the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) c= Funcs ( the carrier of X, the carrier of (M -TOP_prod (M --> Sierpinski_Space))) by Th32;
now__::_thesis:_for_a_being_Element_of_(oContMaps_(X,(M_-TOP_prod_(M_-->_Sierpinski_Space))))_holds_(G_*_F)_._a_=_(id_(oContMaps_(X,(M_-TOP_prod_(M_-->_Sierpinski_Space)))))_._a
let a be Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))); ::_thesis: (G * F) . a = (id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) . a
 a in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) ;
then A15: commute (commute a) = a by A14, A13, FUNCT_6:57;
thus (G * F) . a = G . (F . a) by FUNCT_2:15
.= commute (F . a) by A5
.= a by A1, A15
.= (id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))))) . a by FUNCT_1:18 ; ::_thesis: verum
end;
then A16: G * F = id (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by FUNCT_2:63;
A17: RelStr(# the carrier of (Omega (M -TOP_prod (M --> Sierpinski_Space))), the InternalRel of (Omega (M -TOP_prod (M --> Sierpinski_Space))) #) = M -POS_prod (M --> (Omega Sierpinski_Space)) by WAYBEL25:14;
A18: F is monotone
proof
let a, b be Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))); :: according to WAYBEL_1:def_2 ::_thesis: ( not a <= b or F . a <= F . b )
assume A19: a <= b ; ::_thesis: F . a <= F . b
reconsider f9 = a, g9 = b as continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) by Th2;
reconsider f = a, g = b as continuous Function of X,(Omega (M -TOP_prod (M --> Sierpinski_Space))) by Th1;
now__::_thesis:_for_i_being_Element_of_M_holds_(F_._a)_._i_<=_(F_._b)_._i
let i be Element of M; ::_thesis: (F . a) . i <= (F . b) . i
A20: (M --> (oContMaps (X,Sierpinski_Space))) . i = oContMaps (X,Sierpinski_Space) by FUNCOP_1:7;
then reconsider Fai = (F . a) . i, Fbi = (F . b) . i as continuous Function of X,(Omega Sierpinski_Space) by Th1;
now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_X_holds_
ex_a,_b_being_Element_of_(Omega_Sierpinski_Space)_st_
(_a_=_Fai_._j_&_b_=_Fbi_._j_&_a_<=_b_)
let j be set ; ::_thesis: ( j in the carrier of X implies ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b ) )
assume  j in the carrier of X ; ::_thesis: ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b )
then reconsider x = j as Element of X ;
 ( b in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) & F . b = commute g ) by A1;
then A21: Fbi . x = (g9 . x) . i by A14, A13, FUNCT_6:56;
reconsider fx = f . x, gx = g . x as Element of (M -POS_prod (M --> (Omega Sierpinski_Space))) by A17;
 ( a in the carrier of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) & F . a = commute f ) by A1;
then A22: Fai . x = (f9 . x) . i by A14, A13, FUNCT_6:56;
 f <= g by A19, Th3;
then  ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . x & b = g . x & a <= b ) by YELLOW_2:def_1;
then  fx <= gx by A17, YELLOW_0:1;
then A23: fx . i <= gx . i by WAYBEL_3:28;
 (M --> (Omega Sierpinski_Space)) . i = Omega Sierpinski_Space by FUNCOP_1:7;
hence  ex a, b being Element of (Omega Sierpinski_Space) st
( a = Fai . j & b = Fbi . j & a <= b ) by A22, A21, A23; ::_thesis: verum
end;
then  Fai <= Fbi by YELLOW_2:def_1;
hence  (F . a) . i <= (F . b) . i by A20, Th3; ::_thesis: verum
end;
hence  F . a <= F . b by WAYBEL_3:28; ::_thesis: verum
end;
A24: the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) = the carrier of ((oContMaps (X,Sierpinski_Space)) |^ M) by YELLOW_1:def_5
.= Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) by YELLOW_1:28 ;
then A25: the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) c= Funcs (M,(Funcs ( the carrier of X, the carrier of Sierpinski_Space))) by Th32, FUNCT_5:56;
A26: G is monotone
proof
let a, b be Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))); :: according to WAYBEL_1:def_2 ::_thesis: ( not a <= b or G . a <= G . b )
assume A27: a <= b ; ::_thesis: G . a <= G . b
reconsider f = G . a, g = G . b as continuous Function of X,(Omega (M -TOP_prod (M --> Sierpinski_Space))) by Th1;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_X_holds_
ex_a,_b_being_Element_of_(Omega_(M_-TOP_prod_(M_-->_Sierpinski_Space)))_st_
(_a_=_f_._i_&_b_=_g_._i_&_a_<=_b_)
let i be set ; ::_thesis: ( i in the carrier of X implies ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b ) )
assume  i in the carrier of X ; ::_thesis: ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b )
then reconsider x = i as Element of X ;
reconsider fx = f . x, gx = g . x as Element of (M -POS_prod (M --> (Omega Sierpinski_Space))) by A17;
now__::_thesis:_for_j_being_Element_of_M_holds_fx_._j_<=_gx_._j
let j be Element of M; ::_thesis: fx . j <= gx . j
A28: (M --> (oContMaps (X,Sierpinski_Space))) . j = oContMaps (X,Sierpinski_Space) by FUNCOP_1:7;
then reconsider aj = a . j, bj = b . j as continuous Function of X,(Omega Sierpinski_Space) by Th1;
 a . j <= b . j by A27, WAYBEL_3:28;
then  aj <= bj by A28, Th3;
then A29: ex a, b being Element of (Omega Sierpinski_Space) st
( a = aj . x & b = bj . x & a <= b ) by YELLOW_2:def_1;
 ( b in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) & G . b = commute b ) by A5;
then A30: gx . j = bj . x by A25, FUNCT_6:56;
 ( a in the carrier of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) & G . a = commute a ) by A5;
then  fx . j = aj . x by A25, FUNCT_6:56;
hence  fx . j <= gx . j by A30, A29, FUNCOP_1:7; ::_thesis: verum
end;
then  fx <= gx by WAYBEL_3:28;
hence  ex a, b being Element of (Omega (M -TOP_prod (M --> Sierpinski_Space))) st
( a = f . i & b = g . i & a <= b ) by A17, YELLOW_0:1; ::_thesis: verum
end;
then  f <= g by YELLOW_2:def_1;
hence  G . a <= G . b by Th3; ::_thesis: verum
end;
now__::_thesis:_for_a_being_Element_of_(M_-POS_prod_(M_-->_(oContMaps_(X,Sierpinski_Space))))_holds_(F_*_G)_._a_=_(id_(M_-POS_prod_(M_-->_(oContMaps_(X,Sierpinski_Space)))))_._a
let a be Element of (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))); ::_thesis: (F * G) . a = (id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) . a
 ( a in Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) & Funcs (M, the carrier of (oContMaps (X,Sierpinski_Space))) c= Funcs (M,(Funcs ( the carrier of X, the carrier of Sierpinski_Space))) ) by A24, Th32, FUNCT_5:56;
then A31: commute (commute a) = a by FUNCT_6:57;
thus (F * G) . a = F . (G . a) by FUNCT_2:15
.= commute (G . a) by A1
.= a by A5, A31
.= (id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))))) . a by FUNCT_1:18 ; ::_thesis: verum
end;
then  F * G = id (M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) by FUNCT_2:63;
hence  F is isomorphic by A18, A26, A16, YELLOW16:15; ::_thesis: for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f
let f be continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)); ::_thesis: F . f = commute f
 f is Element of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))) by Th2;
hence  F . f = commute f by A1; ::_thesis: verum
end;

theorem Th35: :: WAYBEL26:35
for X being non empty TopSpace
for M being non empty set holds oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))),M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))) are_isomorphic
proof
let X be non empty TopSpace; ::_thesis: for M being non empty set holds oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))),M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))) are_isomorphic
let M be non empty set ; ::_thesis: oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))),M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))) are_isomorphic
consider F being Function of (oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space)))),(M -POS_prod (M --> (oContMaps (X,Sierpinski_Space)))) such that
A1: F is isomorphic and
 for f being continuous Function of X,(M -TOP_prod (M --> Sierpinski_Space)) holds F . f = commute f by Th34;
take  F ; :: according to WAYBEL_1:def_8 ::_thesis: F is isomorphic
thus  F is isomorphic by A1; ::_thesis: verum
end;

theorem Th36: :: WAYBEL26:36
for X being non empty TopSpace st InclPoset the topology of X is continuous holds
for Y being injective T_0-TopSpace holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
proof
let X be non empty TopSpace; ::_thesis: ( InclPoset the topology of X is continuous implies for Y being injective T_0-TopSpace holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) )
assume A1: InclPoset the topology of X is continuous ; ::_thesis: for Y being injective T_0-TopSpace holds
( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
 InclPoset the topology of X, oContMaps (X,Sierpinski_Space) are_isomorphic by Th6;
then reconsider XS = oContMaps (X,Sierpinski_Space) as non empty complete continuous Poset by A1, WAYBEL15:9, WAYBEL20:18;
let Y be injective T_0-TopSpace; ::_thesis: ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous )
consider M being non empty set  such that
A2: Y is_Retract_of M -TOP_prod (M --> Sierpinski_Space) by WAYBEL18:19;
 for i being Element of M holds (M --> Sierpinski_Space) . i is injective by FUNCOP_1:7;
then reconsider MS = M -TOP_prod (M --> Sierpinski_Space) as injective T_0-TopSpace by WAYBEL18:7;
 for i being Element of M holds (M --> XS) . i is complete continuous LATTICE by FUNCOP_1:7;
then A3: ( M -POS_prod (M --> XS) is complete & M -POS_prod (M --> XS) is continuous ) by WAYBEL20:33;
 M -POS_prod (M --> (oContMaps (X,Sierpinski_Space))), oContMaps (X,(M -TOP_prod (M --> Sierpinski_Space))) are_isomorphic by Th35, WAYBEL_1:6;
then  ( oContMaps (X,MS) is complete & oContMaps (X,MS) is continuous ) by A3, WAYBEL15:9, WAYBEL20:18;
hence  ( oContMaps (X,Y) is complete & oContMaps (X,Y) is continuous ) by A2, Th23; ::_thesis: verum
end;

registration
cluster non empty non trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott for TopRelStr ;
existence
 ex b1 being TopLattice st
( not b1 is trivial & b1 is complete & b1 is Scott )
proof
set L = BoolePoset 1;
set T = the Scott TopAugmentation of BoolePoset 1;
take  the Scott TopAugmentation of BoolePoset 1 ; ::_thesis: ( not the Scott TopAugmentation of BoolePoset 1 is trivial & the Scott TopAugmentation of BoolePoset 1 is complete & the Scott TopAugmentation of BoolePoset 1 is Scott )
 ( BoolePoset 1 = InclPoset (bool 1) & RelStr(# the carrier of the Scott TopAugmentation of BoolePoset 1, the InternalRel of the Scott TopAugmentation of BoolePoset 1 #) = RelStr(# the carrier of (BoolePoset 1), the InternalRel of (BoolePoset 1) #) ) by YELLOW_1:4, YELLOW_9:def_4;
then A1: the carrier of the Scott TopAugmentation of BoolePoset 1 = bool 1 by YELLOW_1:1;
 ( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def_2;
hence  ( not the Scott TopAugmentation of BoolePoset 1 is trivial & the Scott TopAugmentation of BoolePoset 1 is complete & the Scott TopAugmentation of BoolePoset 1 is Scott ) by A1, STRUCT_0:def_10, YELLOW14:1; ::_thesis: verum
end;
end;

theorem :: WAYBEL26:37
for X being non empty TopSpace
for L being non trivial complete Scott TopLattice holds
( oContMaps (X,L) is complete & oContMaps (X,L) is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )
proof
let X be non empty TopSpace; ::_thesis: for L being non trivial complete Scott TopLattice holds
( oContMaps (X,L) is complete & oContMaps (X,L) is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )
let L be non trivial complete Scott TopLattice; ::_thesis: ( oContMaps (X,L) is complete & oContMaps (X,L) is continuous iff ( InclPoset the topology of X is continuous & L is continuous ) )
A1: L is Scott TopAugmentation of L by YELLOW_9:44;
 Omega L = TopRelStr(# the carrier of L, the InternalRel of L, the topology of L #) by WAYBEL25:15;
then A2: RelStr(# the carrier of (Omega L), the InternalRel of (Omega L) #) = RelStr(# the carrier of L, the InternalRel of L #) ;
A3: L is monotone-convergence by WAYBEL25:29;
hereby  ::_thesis: ( InclPoset the topology of X is continuous & L is continuous implies ( oContMaps (X,L) is complete & oContMaps (X,L) is continuous ) )
assume A4: ( oContMaps (X,L) is complete & oContMaps (X,L) is continuous ) ; ::_thesis: ( InclPoset the topology of X is continuous & L is continuous )
hence  InclPoset the topology of X is continuous by A3, Th26; ::_thesis: L is continuous
 Omega L is continuous by A1, A4, Th28;
hence  L is continuous by A2, YELLOW12:15; ::_thesis: verum
end;
thus  ( InclPoset the topology of X is continuous & L is continuous implies ( oContMaps (X,L) is complete & oContMaps (X,L) is continuous ) ) by A1, Th36; ::_thesis: verum
end;

registration
let f be Function;
cluster Union (disjoin f) ->  Relation-like ;
coherence
 Union (disjoin f) is Relation-like
proof
 for x being set st x in Union (disjoin f) holds
ex y, z being set st x = [y,z] by CARD_3:21;
hence  Union (disjoin f) is Relation-like by RELAT_1:def_1; ::_thesis: verum
end;
end;

definition
let f be Function;
func *graph f ->  Relation equals :: WAYBEL26:def 4
(Union (disjoin f)) ~ ;
correctness
coherence
(Union (disjoin f)) ~ is Relation;
;
end;

:: deftheorem  defines *graph WAYBEL26:def_4_:_
 for f being Function holds *graph f = (Union (disjoin f)) ~ ;


theorem Th38: :: WAYBEL26:38
for x, y being set
for f being Function holds
( [x,y] in *graph f iff ( x in dom f & y in f . x ) )
proof
let x, y be set ; ::_thesis: for f being Function holds
( [x,y] in *graph f iff ( x in dom f & y in f . x ) )
let f be Function; ::_thesis: ( [x,y] in *graph f iff ( x in dom f & y in f . x ) )
A1: ( [x,y] in *graph f iff [y,x] in Union (disjoin f) ) by RELAT_1:def_7;
 ( [y,x] `1 = y & [y,x] `2 = x ) ;
hence  ( [x,y] in *graph f iff ( x in dom f & y in f . x ) ) by A1, CARD_3:22; ::_thesis: verum
end;

theorem Th39: :: WAYBEL26:39
for X being finite set holds
( proj1 X is finite & proj2 X is finite )
proof
deffunc H1( set ) ->  set = $1 `1 ;
let X be finite set ; ::_thesis: ( proj1 X is finite & proj2 X is finite )
consider f being Function such that
A1: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
A2: proj1 X c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 X or x in rng f )
assume  x in proj1 X ; ::_thesis: x in rng f
then consider y being set  such that
A3: [x,y] in X by XTUPLE_0:def_12;
 [x,y] `1 = x ;
then  f . [x,y] = x by A1, A3;
hence  x in rng f by A1, A3, FUNCT_1:def_3; ::_thesis: verum
end;
 rng f is finite by A1, FINSET_1:8;
hence  proj1 X is finite by A2; ::_thesis: proj2 X is finite
deffunc H2( set ) ->  set = $1 `2 ;
consider f being Function such that
A4: ( dom f = X & ( for x being set st x in X holds
f . x = H2(x) ) ) from FUNCT_1:sch_3();
A5: proj2 X c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj2 X or x in rng f )
assume  x in proj2 X ; ::_thesis: x in rng f
then consider y being set  such that
A6: [y,x] in X by XTUPLE_0:def_13;
 [y,x] `2 = x ;
then  f . [y,x] = x by A4, A6;
hence  x in rng f by A4, A6, FUNCT_1:def_3; ::_thesis: verum
end;
 rng f is finite by A4, FINSET_1:8;
hence  proj2 X is finite by A5; ::_thesis: verum
end;

theorem Th40: :: WAYBEL26:40
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
proof
let X, Y be non empty TopSpace; ::_thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds
f is continuous
let f be Function of X,S; ::_thesis: ( *graph f is open Subset of [:X,Y:] implies f is continuous )
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4;
A2: dom f = the carrier of X by FUNCT_2:def_1;
assume  *graph f is open Subset of [:X,Y:] ; ::_thesis: f is continuous
then consider AA being Subset-Family of [:X,Y:] such that
A3: *graph f = union AA and
A4: for e being set st e in AA holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
A5: the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;
A6: now__::_thesis:_for_P_being_Subset_of_S_st_P_is_open_holds_
f_"_P_is_open
let P be Subset of S; ::_thesis: ( P is open implies f " P is open )
assume A7: P is open ; ::_thesis: f " P is open
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_f_"_P_implies_ex_Q_being_Subset_of_X_st_
(_Q_is_open_&_Q_c=_f_"_P_&_x_in_Q_)_)_&_(_ex_Q_being_Subset_of_X_st_
(_Q_is_open_&_Q_c=_f_"_P_&_x_in_Q_)_implies_x_in_f_"_P_)_)
let x be set ; ::_thesis: ( ( x in f " P implies ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )
hereby  ::_thesis: ( ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) implies x in f " P )
defpred S1[ set , set ] means ( x in $2 `1 & $1 in $2 `2 & [:($2 `1),($2 `2):] c= *graph f );
assume A8: x in f " P ; ::_thesis: ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q )
then reconsider y = x as Element of X ;
A9: now__::_thesis:_for_e_being_set_st_e_in_f_._x_holds_
ex_u_being_set_st_
(_u_in_[:_the_topology_of_X,_the_topology_of_Y:]_&_S1[e,u]_)
let e be set ; ::_thesis: ( e in f . x implies ex u being set st
( u in [: the topology of X, the topology of Y:] & S1[e,u] ) )
assume  e in f . x ; ::_thesis: ex u being set st
( u in [: the topology of X, the topology of Y:] & S1[e,u] )
then  [x,e] in *graph f by A2, A8, Th38;
then consider V being set  such that
A10: [x,e] in V and
A11: V in AA by A3, TARSKI:def_4;
consider A being Subset of X, B being Subset of Y such that
A12: V = [:A,B:] and
A13: ( A is open & B is open ) by A4, A11;
reconsider u = [A,B] as set ;
take u = u; ::_thesis: ( u in [: the topology of X, the topology of Y:] & S1[e,u] )
 ( A in the topology of X & B in the topology of Y ) by A13, PRE_TOPC:def_2;
hence  u in [: the topology of X, the topology of Y:] by ZFMISC_1:87; ::_thesis: S1[e,u]
 ( A = u `1 & B = u `2 ) by MCART_1:7;
hence  S1[e,u] by A3, A10, A11, A12, ZFMISC_1:74, ZFMISC_1:87; ::_thesis: verum
end;
consider g being Function such that
A14: ( dom g = f . x & rng g c= [: the topology of X, the topology of Y:] ) and
A15: for a being set st a in f . x holds
S1[a,g . a] from FUNCT_1:sch_5(A9);
set J =  {  (union A) where A is Subset of (proj2 (rng g)) : A is finite  }  ;
A16: proj2 (rng g) c= the topology of Y by A14, FUNCT_5:11;
A17:  {  (union A) where A is Subset of (proj2 (rng g)) : A is finite  }  c= the topology of Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (union A) where A is Subset of (proj2 (rng g)) : A is finite  }  or x in the topology of Y )
assume  x in  {  (union A) where A is Subset of (proj2 (rng g)) : A is finite  }  ; ::_thesis: x in the topology of Y
then consider A being Subset of (proj2 (rng g)) such that
A18: x = union A and
 A is finite ;
A19: A c= the topology of Y by A16, XBOOLE_1:1;
then  A is Subset-Family of Y by XBOOLE_1:1;
hence  x in the topology of Y by A18, A19, PRE_TOPC:def_1; ::_thesis: verum
end;
 {} (proj2 (rng g)) in  {  (union A) where A is Subset of (proj2 (rng g)) : A is finite  }  by ZFMISC_1:2;
then reconsider J =  {  (union A) where A is Subset of (proj2 (rng g)) : A is finite  }  as non empty Subset of (InclPoset the topology of Y) by A17, YELLOW_1:1;
 J is directed
proof
let a, b be Element of (InclPoset the topology of Y); :: according to WAYBEL_0:def_1 ::_thesis: ( not a in J or not b in J or ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in J & a <= b1 & b <= b1 ) )
assume  a in J ; ::_thesis: ( not b in J or ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in J & a <= b1 & b <= b1 ) )
then consider A being Subset of (proj2 (rng g)) such that
A20: a = union A and
A21: A is finite ;
assume  b in J ; ::_thesis: ex b1 being Element of the carrier of (InclPoset the topology of Y) st
( b1 in J & a <= b1 & b <= b1 )
then consider B being Subset of (proj2 (rng g)) such that
A22: b = union B and
A23: B is finite ;
reconsider AB = A \/ B as finite Subset of (proj2 (rng g)) by A21, A23;
take ab = a "\/" b; ::_thesis: ( ab in J & a <= ab & b <= ab )
A24: a \/ b = ab by WAYBEL14:18;
 union AB = a \/ b by A20, A22, ZFMISC_1:78;
hence  ab in J by A24; ::_thesis: ( a <= ab & b <= ab )
 ( a c= ab & b c= ab ) by A24, XBOOLE_1:7;
hence  ( a <= ab & b <= ab ) by YELLOW_1:3; ::_thesis: verum
end;
then reconsider J9 = J as non empty directed Subset of S by A1, WAYBEL_0:3;
A25: proj2 (rng g) c= bool (f . x)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in proj2 (rng g) or z in bool (f . x) )
assume  z in proj2 (rng g) ; ::_thesis: z in bool (f . x)
then consider z1 being set  such that
A26: [z1,z] in rng g by XTUPLE_0:def_13;
A27: [z1,z] `1 = z1 ;
A28: ex a being set st
( a in dom g & [z1,z] = g . a ) by A26, FUNCT_1:def_3;
then A29: x in z1 by A14, A15, A27;
 [z1,z] `2 = z ;
then A30: [:z1,z:] c= *graph f by A14, A15, A28, A27;
 z c= f . x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in z or a in f . x )
assume  a in z ; ::_thesis: a in f . x
then  [x,a] in [:z1,z:] by A29, ZFMISC_1:87;
hence  a in f . x by A30, Th38; ::_thesis: verum
end;
hence  z in bool (f . x) ; ::_thesis: verum
end;
 union J = f . y
proof
thus  union J c= f . y :: according to XBOOLE_0:def_10 ::_thesis: f . y c= union J
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union J or a in f . y )
assume  a in union J ; ::_thesis: a in f . y
then consider u being set  such that
A31: a in u and
A32: u in J by TARSKI:def_4;
consider A being Subset of (proj2 (rng g)) such that
A33: u = union A and
 A is finite by A32;
 A c= bool (f . y) by A25, XBOOLE_1:1;
then  u c= union (bool (f . y)) by A33, ZFMISC_1:77;
then  u c= f . y by ZFMISC_1:81;
hence  a in f . y by A31; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f . y or a in union J )
assume A34: a in f . y ; ::_thesis: a in union J
then A35: g . a in rng g by A14, FUNCT_1:def_3;
then  g . a = [((g . a) `1),((g . a) `2)] by A14, MCART_1:21;
then  (g . a) `2 in proj2 (rng g) by A35, XTUPLE_0:def_13;
then reconsider A = {((g . a) `2)} as Subset of (proj2 (rng g)) by ZFMISC_1:31;
 union A = (g . a) `2 by ZFMISC_1:25;
then A36: (g . a) `2 in J ;
 a in (g . a) `2 by A15, A34;
hence  a in union J by A36, TARSKI:def_4; ::_thesis: verum
end;
then  sup J = f . y by YELLOW_1:22;
then A37: sup J9 = f . y by A1, YELLOW_0:17, YELLOW_0:26;
 f . y in the topology of Y by A5, A1;
then reconsider W = f . y as open Subset of Y by PRE_TOPC:def_2;
A38: proj1 (rng g) c= the topology of X by A14, FUNCT_5:11;
defpred S2[ set , set ] means  ex c1 being set st
( [c1,$1] = g . $2 & x in c1 & $2 in $1 & $2 in f . x & [:c1,$1:] c= *graph f );
 f . x in P by A8, FUNCT_2:38;
then  J meets P by A7, A37, WAYBEL11:def_1;
then consider a being set  such that
A39: a in J and
A40: a in P by XBOOLE_0:3;
reconsider a = a as Element of S by A40;
consider A being Subset of (proj2 (rng g)) such that
A41: a = union A and
A42: A is finite by A39;
A43: now__::_thesis:_for_c_being_set_st_c_in_A_holds_
ex_a_being_set_st_
(_a_in_W_&_S2[c,a]_)
let c be set ; ::_thesis: ( c in A implies ex a being set st
( a in W & S2[c,a] ) )
assume  c in A ; ::_thesis: ex a being set st
( a in W & S2[c,a] )
then consider c1 being set  such that
A44: [c1,c] in rng g by XTUPLE_0:def_13;
consider a being set  such that
A45: a in dom g and
A46: [c1,c] = g . a by A44, FUNCT_1:def_3;
take a = a; ::_thesis: ( a in W & S2[c,a] )
thus  a in W by A14, A45; ::_thesis: S2[c,a]
A47: [c1,c] `1 = c1 ;
then A48: x in c1 by A14, A15, A45, A46;
A49: [c1,c] `2 = c ;
then  [:c1,c:] c= *graph f by A14, A15, A45, A46, A47;
hence  S2[c,a] by A14, A15, A45, A46, A49, A48; ::_thesis: verum
end;
consider hh being Function such that
A50: ( dom hh = A & rng hh c= W ) and
A51: for c being set st c in A holds
S2[c,hh . c] from FUNCT_1:sch_5(A43);
set B = proj1 (g .: (rng hh));
 g .: (rng hh) c= rng g by RELAT_1:111;
then  proj1 (g .: (rng hh)) c= proj1 (rng g) by XTUPLE_0:8;
then A52: proj1 (g .: (rng hh)) c= the topology of X by A38, XBOOLE_1:1;
then reconsider B = proj1 (g .: (rng hh)) as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
reconsider Q = Intersect B as Subset of X ;
take Q = Q; ::_thesis: ( Q is open & Q c= f " P & x in Q )
 g .: (rng hh) is finite by A42, A50, FINSET_1:5, FINSET_1:8;
then  B is finite by Th39;
then  Q in FinMeetCl the topology of X by A52, CANTOR_1:def_3;
then  Q in the topology of X by CANTOR_1:5;
hence  Q is open by PRE_TOPC:def_2; ::_thesis: ( Q c= f " P & x in Q )
thus  Q c= f " P ::_thesis: x in Q
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Q or z in f " P )
assume A53: z in Q ; ::_thesis: z in f " P
then reconsider zz = z as Element of X ;
reconsider fz = f . zz, aa = a as Element of (InclPoset the topology of Y) by A1;
 a c= f . zz
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in a or p in f . zz )
assume  p in a ; ::_thesis: p in f . zz
then consider q being set  such that
A54: p in q and
A55: q in A by A41, TARSKI:def_4;
consider q1 being set  such that
A56: [q1,q] = g . (hh . q) and
 x in q1 and
 hh . q in q and
A57: hh . q in f . x and
A58: [:q1,q:] c= *graph f by A51, A55;
 hh . q in rng hh by A50, A55, FUNCT_1:def_3;
then  [q1,q] in g .: (rng hh) by A14, A56, A57, FUNCT_1:def_6;
then  q1 in B by XTUPLE_0:def_12;
then  zz in q1 by A53, SETFAM_1:43;
then  [zz,p] in [:q1,q:] by A54, ZFMISC_1:87;
hence  p in f . zz by A58, Th38; ::_thesis: verum
end;
then  aa <= fz by YELLOW_1:3;
then  a <= f . zz by A1, YELLOW_0:1;
then  f . zz in P by A7, A40, WAYBEL_0:def_20;
hence  z in f " P by FUNCT_2:38; ::_thesis: verum
end;
now__::_thesis:_for_c1_being_set_st_c1_in_B_holds_
x_in_c1
let c1 be set ; ::_thesis: ( c1 in B implies x in c1 )
assume  c1 in B ; ::_thesis: x in c1
then consider c being set  such that
A59: [c1,c] in g .: (rng hh) by XTUPLE_0:def_12;
consider b being set  such that
 b in dom g and
A60: b in rng hh and
A61: [c1,c] = g . b by A59, FUNCT_1:def_6;
consider c9 being set  such that
A62: c9 in dom hh and
A63: b = hh . c9 by A60, FUNCT_1:def_3;
 ex c91 being set st
( [c91,c9] = g . (hh . c9) & x in c91 & hh . c9 in c9 & hh . c9 in f . x & [:c91,c9:] c= *graph f ) by A50, A51, A62;
hence  x in c1 by A61, A63, XTUPLE_0:1; ::_thesis: verum
end;
hence  x in Q by A8, SETFAM_1:43; ::_thesis: verum
end;
assume  ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ; ::_thesis: x in f " P
hence  x in f " P ; ::_thesis: verum
end;
hence  f " P is open by TOPS_1:25; ::_thesis: verum
end;
 [#] S <> {} ;
hence  f is continuous by A6, TOPS_2:43; ::_thesis: verum
end;

definition
let W be Relation;
let X be set ;
func(W,X) *graph  ->  Function means :Def5: :: WAYBEL26:def 5
( dom it = X & ( for x being set st x in X holds
it . x = Im (W,x) ) );
existence
 ex b1 being Function st
( dom b1 = X & ( for x being set st x in X holds
b1 . x = Im (W,x) ) )
proof
deffunc H1( set ) ->  set = Im (W,$1);
thus  ex f being Function st
( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3(); ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function st dom b1 = X & ( for x being set st x in X holds
b1 . x = Im (W,x) ) & dom b2 = X & ( for x being set st x in X holds
b2 . x = Im (W,x) ) holds
b1 = b2;
proof
let f, g be Function; ::_thesis: ( dom f = X & ( for x being set st x in X holds
f . x = Im (W,x) ) & dom g = X & ( for x being set st x in X holds
g . x = Im (W,x) ) implies f = g )
assume that
A1: dom f = X and
A2: for x being set st x in X holds
f . x = Im (W,x) and
A3: dom g = X and
A4: for x being set st x in X holds
g . x = Im (W,x) ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in X implies f . x = g . x )
assume A5: x in X ; ::_thesis: f . x = g . x
hence f . x = Im (W,x) by A2
.= g . x by A4, A5 ;
::_thesis: verum
end;
hence  f = g by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines *graph WAYBEL26:def_5_:_
 for W being Relation
for X being set
for b3 being Function holds
( b3 = (W,X) *graph iff ( dom b3 = X & ( for x being set st x in X holds
b3 . x = Im (W,x) ) ) );

theorem Th41: :: WAYBEL26:41
for W being Relation
for X being set st dom W c= X holds
*graph ((W,X) *graph) = W
proof
let W be Relation; ::_thesis: for X being set st dom W c= X holds
*graph ((W,X) *graph) = W
let X be set ; ::_thesis: ( dom W c= X implies *graph ((W,X) *graph) = W )
assume A1: dom W c= X ; ::_thesis: *graph ((W,X) *graph) = W
A2: dom ((W,X) *graph) = X by Def5;
now__::_thesis:_for_x,_y_being_set_holds_
(_(_[x,y]_in_*graph_((W,X)_*graph)_implies_[x,y]_in_W_)_&_(_[x,y]_in_W_implies_[x,y]_in_*graph_((W,X)_*graph)_)_)
let x, y be set ; ::_thesis: ( ( [x,y] in *graph ((W,X) *graph) implies [x,y] in W ) & ( [x,y] in W implies [x,y] in *graph ((W,X) *graph) ) )
hereby  ::_thesis: ( [x,y] in W implies [x,y] in *graph ((W,X) *graph) )
assume  [x,y] in *graph ((W,X) *graph) ; ::_thesis: [x,y] in W
then  ( x in X & y in ((W,X) *graph) . x ) by A2, Th38;
then  y in Im (W,x) by Def5;
then  ex z being set st
( [z,y] in W & z in {x} ) by RELAT_1:def_13;
hence  [x,y] in W by TARSKI:def_1; ::_thesis: verum
end;
assume A3: [x,y] in W ; ::_thesis: [x,y] in *graph ((W,X) *graph)
then A4: x in dom W by XTUPLE_0:def_12;
 x in {x} by TARSKI:def_1;
then  y in Im (W,x) by A3, RELAT_1:def_13;
then  y in ((W,X) *graph) . x by A1, A4, Def5;
hence  [x,y] in *graph ((W,X) *graph) by A1, A2, A4, Th38; ::_thesis: verum
end;
hence  *graph ((W,X) *graph) = W by RELAT_1:def_2; ::_thesis: verum
end;

registration
let X, Y be TopSpace;
cluster  ->  Relation-like for Element of bool the carrier of [:X,Y:];
coherence
 for b1 being Subset of [:X,Y:] holds b1 is Relation-like
proof
let r be Subset of [:X,Y:]; ::_thesis: r is Relation-like
 r is Subset of [: the carrier of X, the carrier of Y:] by BORSUK_1:def_2;
hence  r is Relation-like ; ::_thesis: verum
end;
cluster  ->  Relation-like for Element of the topology of [:X,Y:];
coherence
 for b1 being Element of the topology of [:X,Y:] holds b1 is Relation-like ;
end;

theorem Th42: :: WAYBEL26:42
for X, Y being non empty TopSpace
for W being open Subset of [:X,Y:]
for x being Point of X holds Im (W,x) is open Subset of Y
proof
let X, Y be non empty TopSpace; ::_thesis: for W being open Subset of [:X,Y:]
for x being Point of X holds Im (W,x) is open Subset of Y
let W be open Subset of [:X,Y:]; ::_thesis: for x being Point of X holds Im (W,x) is open Subset of Y
let x be Point of X; ::_thesis: Im (W,x) is open Subset of Y
reconsider W = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def_2;
reconsider A = W .: {x} as Subset of Y ;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_A_implies_ex_Y1_being_Subset_of_Y_st_
(_Y1_is_open_&_Y1_c=_A_&_y_in_Y1_)_)_&_(_ex_Q_being_Subset_of_Y_st_
(_Q_is_open_&_Q_c=_A_&_y_in_Q_)_implies_y_in_A_)_)
let y be set ; ::_thesis: ( ( y in A implies ex Y1 being Subset of Y st
( Y1 is open & Y1 c= A & y in Y1 ) ) & ( ex Q being Subset of Y st
( Q is open & Q c= A & y in Q ) implies y in A ) )
hereby  ::_thesis: ( ex Q being Subset of Y st
( Q is open & Q c= A & y in Q ) implies y in A )
assume  y in A ; ::_thesis: ex Y1 being Subset of Y st
( Y1 is open & Y1 c= A & y in Y1 )
then consider z being set  such that
A1: [z,y] in W and
A2: z in {x} by RELAT_1:def_13;
consider AA being Subset-Family of [:X,Y:] such that
A3: W = union AA and
A4: for e being set st e in AA holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
 z = x by A2, TARSKI:def_1;
then consider e being set  such that
A5: [x,y] in e and
A6: e in AA by A1, A3, TARSKI:def_4;
consider X1 being Subset of X, Y1 being Subset of Y such that
A7: e = [:X1,Y1:] and
 X1 is open and
A8: Y1 is open by A4, A6;
take Y1 = Y1; ::_thesis: ( Y1 is open & Y1 c= A & y in Y1 )
thus  Y1 is open by A8; ::_thesis: ( Y1 c= A & y in Y1 )
A9: x in X1 by A5, A7, ZFMISC_1:87;
thus  Y1 c= A ::_thesis: y in Y1
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Y1 or z in A )
assume  z in Y1 ; ::_thesis: z in A
then  [x,z] in e by A7, A9, ZFMISC_1:87;
then A10: [x,z] in W by A3, A6, TARSKI:def_4;
 x in {x} by TARSKI:def_1;
hence  z in A by A10, RELAT_1:def_13; ::_thesis: verum
end;
thus  y in Y1 by A5, A7, ZFMISC_1:87; ::_thesis: verum
end;
thus  ( ex Q being Subset of Y st
( Q is open & Q c= A & y in Q ) implies y in A ) ; ::_thesis: verum
end;
hence  Im (W,x) is open Subset of Y by TOPS_1:25; ::_thesis: verum
end;

theorem Th43: :: WAYBEL26:43
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W being open Subset of [:X,Y:] holds (W, the carrier of X) *graph is continuous Function of X,S
proof
let X, Y be non empty TopSpace; ::_thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for W being open Subset of [:X,Y:] holds (W, the carrier of X) *graph is continuous Function of X,S
let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for W being open Subset of [:X,Y:] holds (W, the carrier of X) *graph is continuous Function of X,S
let W be open Subset of [:X,Y:]; ::_thesis: (W, the carrier of X) *graph is continuous Function of X,S
set f = (W, the carrier of X) *graph ;
reconsider W = W as Relation of the carrier of X, the carrier of Y by BORSUK_1:def_2;
A1: dom ((W, the carrier of X) *graph) = the carrier of X by Def5;
A2: ( the carrier of (InclPoset the topology of Y) = the topology of Y & RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) ) by YELLOW_1:1, YELLOW_9:def_4;
 rng ((W, the carrier of X) *graph) c= the carrier of S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((W, the carrier of X) *graph) or y in the carrier of S )
assume  y in rng ((W, the carrier of X) *graph) ; ::_thesis: y in the carrier of S
then consider x being set  such that
A3: x in dom ((W, the carrier of X) *graph) and
A4: y = ((W, the carrier of X) *graph) . x by FUNCT_1:def_3;
reconsider x = x as Element of X by A3, Def5;
 y = Im (W,x) by A4, Def5;
then  y is open Subset of Y by Th42;
hence  y in the carrier of S by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider f = (W, the carrier of X) *graph as Function of X,S by A1, FUNCT_2:2;
 dom W c= the carrier of X ;
then  *graph f = W by Th41;
hence  (W, the carrier of X) *graph is continuous Function of X,S by Th40; ::_thesis: verum
end;

theorem Th44: :: WAYBEL26:44
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y
for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds
for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds
f1 <= f2
proof
let X, Y be non empty TopSpace; ::_thesis: for S being Scott TopAugmentation of InclPoset the topology of Y
for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds
for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds
f1 <= f2
let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: for W1, W2 being open Subset of [:X,Y:] st W1 c= W2 holds
for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds
f1 <= f2
let W1, W2 be open Subset of [:X,Y:]; ::_thesis: ( W1 c= W2 implies for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds
f1 <= f2 )
assume A1: W1 c= W2 ; ::_thesis: for f1, f2 being Element of (oContMaps (X,S)) st f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph holds
f1 <= f2
let f1, f2 be Element of (oContMaps (X,S)); ::_thesis: ( f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph implies f1 <= f2 )
assume A2: ( f1 = (W1, the carrier of X) *graph & f2 = (W2, the carrier of X) *graph ) ; ::_thesis: f1 <= f2
reconsider g1 = f1, g2 = f2 as continuous Function of X,(Omega S) by Th1;
 S is TopAugmentation of S by YELLOW_9:44;
then A3: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) by WAYBEL25:16;
A4: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def_4;
now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_X_holds_
ex_a,_b_being_Element_of_the_carrier_of_(Omega_S)_st_
(_a_=_g1_._j_&_b_=_g2_._j_&_a_<=_b_)
let j be set ; ::_thesis: ( j in the carrier of X implies ex a, b being Element of the carrier of (Omega S) st
( a = g1 . j & b = g2 . j & a <= b ) )
assume  j in the carrier of X ; ::_thesis: ex a, b being Element of the carrier of (Omega S) st
( a = g1 . j & b = g2 . j & a <= b )
then reconsider x = j as Element of X ;
reconsider g1x = g1 . x, g2x = g2 . x as Element of (InclPoset the topology of Y) by A3, YELLOW_9:def_4;
take a = g1 . x; ::_thesis: ex b being Element of the carrier of (Omega S) st
( a = g1 . j & b = g2 . j & a <= b )
take b = g2 . x; ::_thesis: ( a = g1 . j & b = g2 . j & a <= b )
thus  ( a = g1 . j & b = g2 . j ) ; ::_thesis: a <= b
 ( g1 . x = Im (W1,x) & g2 . x = Im (W2,x) ) by A2, Def5;
then  g1 . x c= g2 . x by A1, RELAT_1:124;
then  g1x <= g2x by YELLOW_1:3;
hence  a <= b by A4, A3, YELLOW_0:1; ::_thesis: verum
end;
then  g1 <= g2 by YELLOW_2:def_1;
hence  f1 <= f2 by Th3; ::_thesis: verum
end;

theorem :: WAYBEL26:45
for X, Y being non empty TopSpace
for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) st
( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
proof
let X, Y be non empty TopSpace; ::_thesis: for S being Scott TopAugmentation of InclPoset the topology of Y ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) st
( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
let S be Scott TopAugmentation of InclPoset the topology of Y; ::_thesis: ex F being Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) st
( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
deffunc H1( Element of the topology of [:X,Y:]) ->  Function = ($1, the carrier of X) *graph ;
consider F being ManySortedSet of the topology of [:X,Y:] such that
A1: for R being Element of the topology of [:X,Y:] holds F . R = H1(R) from PBOOLE:sch_5();
A2: rng F c= the carrier of (oContMaps (X,S))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of (oContMaps (X,S)) )
assume  y in rng F ; ::_thesis: y in the carrier of (oContMaps (X,S))
then consider x being set  such that
A3: x in dom F and
A4: y = F . x by FUNCT_1:def_3;
reconsider x = x as Element of the topology of [:X,Y:] by A3;
A5: x is open Subset of [:X,Y:] by PRE_TOPC:def_2;
 y = (x, the carrier of X) *graph by A1, A4;
then  y is continuous Function of X,S by A5, Th43;
then  y is Element of (oContMaps (X,S)) by Th2;
hence  y in the carrier of (oContMaps (X,S)) ; ::_thesis: verum
end;
A6: dom F = the topology of [:X,Y:] by PARTFUN1:def_2;
A7: the carrier of (InclPoset the topology of [:X,Y:]) = the topology of [:X,Y:] by YELLOW_1:1;
then reconsider F = F as Function of (InclPoset the topology of [:X,Y:]),(oContMaps (X,S)) by A6, A2, FUNCT_2:2;
take  F ; ::_thesis: ( F is monotone & ( for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph ) )
thus  F is monotone ::_thesis: for W being open Subset of [:X,Y:] holds F . W = (W, the carrier of X) *graph
proof
let x, y be Element of (InclPoset the topology of [:X,Y:]); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or F . x <= F . y )
 ( x in the topology of [:X,Y:] & y in the topology of [:X,Y:] ) by A7;
then reconsider W1 = x, W2 = y as open Subset of [:X,Y:] by PRE_TOPC:def_2;
assume  x <= y ; ::_thesis: F . x <= F . y
then A8: W1 c= W2 by YELLOW_1:3;
 ( F . x = (W1, the carrier of X) *graph & F . y = (W2, the carrier of X) *graph ) by A1, A7;
hence  F . x <= F . y by A8, Th44; ::_thesis: verum
end;
let W be open Subset of [:X,Y:]; ::_thesis: F . W = (W, the carrier of X) *graph
 W in the topology of [:X,Y:] by PRE_TOPC:def_2;
hence  F . W = (W, the carrier of X) *graph by A1; ::_thesis: verum
end;