:: 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;