:: WAYBEL24 semantic presentation begin theorem :: WAYBEL24:1 for S, T being up-complete Scott TopLattice for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T proof let S, T be up-complete Scott TopLattice; ::_thesis: for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T let M be Subset of (SCMaps (S,T)); ::_thesis: "\/" (M,(SCMaps (S,T))) is continuous Function of S,T the carrier of (SCMaps (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13; then "\/" (M,(SCMaps (S,T))) in the carrier of (MonMaps (S,T)) by TARSKI:def_3; hence "\/" (M,(SCMaps (S,T))) is continuous Function of S,T by WAYBEL10:9, WAYBEL17:def_2; ::_thesis: verum end; registration let S be non empty RelStr ; let T be non empty reflexive RelStr ; cluster Function-like constant quasi_total -> monotone for Element of bool [: the carrier of S, the carrier of T:]; coherence for b1 being Function of S,T st b1 is constant holds b1 is monotone proof let f be Function of S,T; ::_thesis: ( f is constant implies f is monotone ) assume A1: f is constant ; ::_thesis: f is monotone for x, y being Element of S st x <= y holds f . x <= f . y proof let x, y be Element of S; ::_thesis: ( x <= y implies f . x <= f . y ) assume x <= y ; ::_thesis: f . x <= f . y y in the carrier of S ; then A2: y in dom f by FUNCT_2:def_1; x in the carrier of S ; then x in dom f by FUNCT_2:def_1; hence f . x <= f . y by A1, A2, FUNCT_1:def_10; ::_thesis: verum end; hence f is monotone by WAYBEL_1:def_2; ::_thesis: verum end; end; registration let S be non empty RelStr ; let T be non empty reflexive RelStr ; let a be Element of T; clusterS --> a -> monotone ; coherence S --> a is monotone proof set f = S --> a; for x, y being Element of S st x <= y holds (S --> a) . x <= (S --> a) . y proof let x, y be Element of S; ::_thesis: ( x <= y implies (S --> a) . x <= (S --> a) . y ) assume x <= y ; ::_thesis: (S --> a) . x <= (S --> a) . y (S --> a) . x = ( the carrier of S --> a) . x .= a by FUNCOP_1:7 .= ( the carrier of S --> a) . y by FUNCOP_1:7 .= (S --> a) . y ; hence (S --> a) . x <= (S --> a) . y ; ::_thesis: verum end; hence S --> a is monotone by WAYBEL_1:def_2; ::_thesis: verum end; end; theorem :: WAYBEL24:2 for S being non empty RelStr for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T) proof let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T) let T be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: Bottom (MonMaps (S,T)) = S --> (Bottom T) set L = MonMaps (S,T); reconsider f = S --> (Bottom T) as Element of (MonMaps (S,T)) by WAYBEL10:9; reconsider f9 = f as Function of S,T ; A1: for b being Element of (MonMaps (S,T)) st b is_>=_than {} holds f <= b proof let b be Element of (MonMaps (S,T)); ::_thesis: ( b is_>=_than {} implies f <= b ) assume b is_>=_than {} ; ::_thesis: f <= b reconsider b9 = b as Function of S,T by WAYBEL10:9; reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58; for x being Element of S holds f9 . x <= b9 . x proof let x be Element of S; ::_thesis: f9 . x <= b9 . x f9 . x = ( the carrier of S --> (Bottom T)) . x .= Bottom T by FUNCOP_1:7 ; hence f9 . x <= b9 . x by YELLOW_0:44; ::_thesis: verum end; then f9 <= b9 by YELLOW_2:9; then f99 <= b99 by WAYBEL10:11; hence f <= b by YELLOW_0:60; ::_thesis: verum end; f is_>=_than {} by YELLOW_0:6; then f = "\/" ({},(MonMaps (S,T))) by A1, YELLOW_0:30; hence Bottom (MonMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum end; theorem :: WAYBEL24:3 for S being non empty RelStr for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T) proof let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T) let T be non empty reflexive antisymmetric upper-bounded RelStr ; ::_thesis: Top (MonMaps (S,T)) = S --> (Top T) set L = MonMaps (S,T); reconsider f = S --> (Top T) as Element of (MonMaps (S,T)) by WAYBEL10:9; reconsider f9 = f as Function of S,T ; A1: for b being Element of (MonMaps (S,T)) st b is_<=_than {} holds f >= b proof let b be Element of (MonMaps (S,T)); ::_thesis: ( b is_<=_than {} implies f >= b ) assume b is_<=_than {} ; ::_thesis: f >= b reconsider b9 = b as Function of S,T by WAYBEL10:9; reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58; for x being Element of S holds f9 . x >= b9 . x proof let x be Element of S; ::_thesis: f9 . x >= b9 . x f9 . x = ( the carrier of S --> (Top T)) . x .= Top T by FUNCOP_1:7 ; hence f9 . x >= b9 . x by YELLOW_0:45; ::_thesis: verum end; then f9 >= b9 by YELLOW_2:9; then f99 >= b99 by WAYBEL10:11; hence f >= b by YELLOW_0:60; ::_thesis: verum end; f is_<=_than {} by YELLOW_0:6; then f = "/\" ({},(MonMaps (S,T))) by A1, YELLOW_0:31; hence Top (MonMaps (S,T)) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum end; scheme :: WAYBEL24:sch 1 FuncFraenkelSL{ F1() -> non empty RelStr , F2() -> non empty RelStr , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } : F4() .: { F3(x) where x is Element of F1() : P1[x] } = { (F4() . F3(x)) where x is Element of F1() : P1[x] } provided A1: the carrier of F2() c= dom F4() proof set f = F4(); thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ) assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } then consider z being set such that z in dom F4() and A2: z in { F3(x) where x is Element of F1() : P1[x] } and A3: y = F4() . z by FUNCT_1:def_6; ex x being Element of F1() st ( z = F3(x) & P1[x] ) by A2; hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ) assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] } then consider x being Element of F1() such that A4: y = F4() . F3(x) and A5: P1[x] ; ( F3(x) in the carrier of F2() & F3(x) in { F3(z) where z is Element of F1() : P1[z] } ) by A5; hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A1, A4, FUNCT_1:def_6; ::_thesis: verum end; scheme :: WAYBEL24:sch 2 Fraenkel6A{ F1() -> LATTICE, F2( set ) -> set , P1[ set ], P2[ set ] } : { F2(v1) where v1 is Element of F1() : P1[v1] } = { F2(v2) where v2 is Element of F1() : P2[v2] } provided A1: for v being Element of F1() holds ( P1[v] iff P2[v] ) proof thus { F2(v1) where v1 is Element of F1() : P1[v1] } c= { F2(v2) where v2 is Element of F1() : P2[v2] } :: according to XBOOLE_0:def_10 ::_thesis: { F2(v2) where v2 is Element of F1() : P2[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F2(v1) where v1 is Element of F1() : P1[v1] } or a in { F2(v2) where v2 is Element of F1() : P2[v2] } ) assume a in { F2(v1) where v1 is Element of F1() : P1[v1] } ; ::_thesis: a in { F2(v2) where v2 is Element of F1() : P2[v2] } then consider V1 being Element of F1() such that A2: a = F2(V1) and A3: P1[V1] ; P2[V1] by A1, A3; hence a in { F2(v2) where v2 is Element of F1() : P2[v2] } by A2; ::_thesis: verum end; thus { F2(v2) where v2 is Element of F1() : P2[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F2(v2) where v2 is Element of F1() : P2[v2] } or a in { F2(v1) where v1 is Element of F1() : P1[v1] } ) assume a in { F2(v1) where v1 is Element of F1() : P2[v1] } ; ::_thesis: a in { F2(v1) where v1 is Element of F1() : P1[v1] } then consider V1 being Element of F1() such that A4: a = F2(V1) and A5: P2[V1] ; P1[V1] by A1, A5; hence a in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; ::_thesis: verum end; end; theorem Th4: :: WAYBEL24:4 for S, T being complete LATTICE for f being monotone Function of S,T for x being Element of S holds f . x = sup (f .: (downarrow x)) proof let S, T be complete LATTICE; ::_thesis: for f being monotone Function of S,T for x being Element of S holds f . x = sup (f .: (downarrow x)) let f be monotone Function of S,T; ::_thesis: for x being Element of S holds f . x = sup (f .: (downarrow x)) let x be Element of S; ::_thesis: f . x = sup (f .: (downarrow x)) A1: for b being Element of T st b is_>=_than f .: (downarrow x) holds f . x <= b proof let b be Element of T; ::_thesis: ( b is_>=_than f .: (downarrow x) implies f . x <= b ) x <= x ; then ( dom f = the carrier of S & x in downarrow x ) by FUNCT_2:def_1, WAYBEL_0:17; then A2: f . x in f .: (downarrow x) by FUNCT_1:def_6; assume b is_>=_than f .: (downarrow x) ; ::_thesis: f . x <= b hence f . x <= b by A2, LATTICE3:def_9; ::_thesis: verum end; ( ex_sup_of downarrow x,S & sup (downarrow x) = x ) by WAYBEL_0:34; then downarrow x is_<=_than x by YELLOW_0:30; then f .: (downarrow x) is_<=_than f . x by YELLOW_2:14; hence f . x = sup (f .: (downarrow x)) by A1, YELLOW_0:30; ::_thesis: verum end; theorem :: WAYBEL24:5 for S, T being lower-bounded complete LATTICE for f being monotone Function of S,T for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) proof let S, T be lower-bounded complete LATTICE; ::_thesis: for f being monotone Function of S,T for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) let f be monotone Function of S,T; ::_thesis: for x being Element of S holds f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) let x be Element of S; ::_thesis: f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) deffunc H1( Element of S) -> Element of S = \$1; defpred S1[ Element of S] means \$1 <= x; defpred S2[ Element of S] means ex y1 being Element of S st ( \$1 <= y1 & y1 in {x} ); A1: the carrier of S c= dom f by FUNCT_2:def_1; A2: f .: { H1(w) where w is Element of S : S1[w] } = { (f . H1(w)) where w is Element of S : S1[w] } from WAYBEL24:sch_1(A1); A3: for x2 being Element of S holds ( S1[x2] iff S2[x2] ) proof let x2 be Element of S; ::_thesis: ( S1[x2] iff S2[x2] ) hereby ::_thesis: ( S2[x2] implies S1[x2] ) A4: x in {x} by TARSKI:def_1; assume x2 <= x ; ::_thesis: ex y1 being Element of S st ( x2 <= y1 & y1 in {x} ) hence ex y1 being Element of S st ( x2 <= y1 & y1 in {x} ) by A4; ::_thesis: verum end; given y1 being Element of S such that A5: ( x2 <= y1 & y1 in {x} ) ; ::_thesis: S1[x2] thus S1[x2] by A5, TARSKI:def_1; ::_thesis: verum end; { H1(w) where w is Element of S : S1[w] } = { H1(x1) where x1 is Element of S : S2[x1] } from WAYBEL24:sch_2(A3); then A6: downarrow x = { w where w is Element of S : w <= x } by WAYBEL_0:14; sup (f .: (downarrow x)) = f . x by Th4 .= f . (sup (downarrow x)) by WAYBEL_0:34 ; hence f . x = "\/" ( { (f . w) where w is Element of S : w <= x } ,T) by A2, A6, WAYBEL_0:34; ::_thesis: verum end; theorem Th6: :: WAYBEL24:6 for S being RelStr for T being non empty RelStr for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T proof let S be RelStr ; ::_thesis: for T being non empty RelStr for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T let T be non empty RelStr ; ::_thesis: for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T let F be Subset of (T |^ the carrier of S); ::_thesis: sup F is Function of S,T set f = sup F; sup F in the carrier of (T |^ the carrier of S) ; then sup F in Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28; then ex f9 being Function st ( f9 = sup F & dom f9 = the carrier of S & rng f9 c= the carrier of T ) by FUNCT_2:def_2; hence sup F is Function of S,T by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; begin definition let X1, X2, Y be non empty RelStr ; let f be Function of [:X1,X2:],Y; let x be Element of X1; func Proj (f,x) -> Function of X2,Y equals :: WAYBEL24:def 1 (curry f) . x; correctness coherence (curry f) . x is Function of X2,Y; proof [: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def_2; then curry f is Function of the carrier of X1,(Funcs ( the carrier of X2, the carrier of Y)) by FUNCT_5:67; hence (curry f) . x is Function of X2,Y by FUNCT_2:5, FUNCT_2:66; ::_thesis: verum end; end; :: deftheorem defines Proj WAYBEL24:def_1_:_ for X1, X2, Y being non empty RelStr for f being Function of [:X1,X2:],Y for x being Element of X1 holds Proj (f,x) = (curry f) . x; theorem Th7: :: WAYBEL24:7 for Y, X1, X2 being non empty RelStr for f being Function of [:X1,X2:],Y for x being Element of X1 for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y) proof let Y, X1, X2 be non empty RelStr ; ::_thesis: for f being Function of [:X1,X2:],Y for x being Element of X1 for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y) let f be Function of [:X1,X2:],Y; ::_thesis: for x being Element of X1 for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y) let x be Element of X1; ::_thesis: for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y) let y be Element of X2; ::_thesis: (Proj (f,x)) . y = f . (x,y) dom f = the carrier of [:X1,X2:] by FUNCT_2:def_1 .= [: the carrier of X1, the carrier of X2:] by YELLOW_3:def_2 ; then [x,y] in dom f by ZFMISC_1:87; hence (Proj (f,x)) . y = f . (x,y) by FUNCT_5:20; ::_thesis: verum end; definition let X1, X2, Y be non empty RelStr ; let f be Function of [:X1,X2:],Y; let y be Element of X2; func Proj (f,y) -> Function of X1,Y equals :: WAYBEL24:def 2 (curry' f) . y; correctness coherence (curry' f) . y is Function of X1,Y; proof [: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def_2; then curry' f is Function of the carrier of X2,(Funcs ( the carrier of X1, the carrier of Y)) by FUNCT_5:68; hence (curry' f) . y is Function of X1,Y by FUNCT_2:5, FUNCT_2:66; ::_thesis: verum end; end; :: deftheorem defines Proj WAYBEL24:def_2_:_ for X1, X2, Y being non empty RelStr for f being Function of [:X1,X2:],Y for y being Element of X2 holds Proj (f,y) = (curry' f) . y; theorem Th8: :: WAYBEL24:8 for Y, X2, X1 being non empty RelStr for f being Function of [:X1,X2:],Y for y being Element of X2 for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y) proof let Y, X2, X1 be non empty RelStr ; ::_thesis: for f being Function of [:X1,X2:],Y for y being Element of X2 for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y) let f be Function of [:X1,X2:],Y; ::_thesis: for y being Element of X2 for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y) let y be Element of X2; ::_thesis: for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y) let x be Element of X1; ::_thesis: (Proj (f,y)) . x = f . (x,y) dom f = the carrier of [:X1,X2:] by FUNCT_2:def_1 .= [: the carrier of X1, the carrier of X2:] by YELLOW_3:def_2 ; then [x,y] in dom f by ZFMISC_1:87; hence (Proj (f,y)) . x = f . (x,y) by FUNCT_5:22; ::_thesis: verum end; theorem Th9: :: WAYBEL24:9 for R, S, T being non empty RelStr for f being Function of [:R,S:],T for a being Element of R for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a proof let R, S, T be non empty RelStr ; ::_thesis: for f being Function of [:R,S:],T for a being Element of R for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a let f be Function of [:R,S:],T; ::_thesis: for a being Element of R for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a let a be Element of R; ::_thesis: for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a let b be Element of S; ::_thesis: (Proj (f,a)) . b = (Proj (f,b)) . a (Proj (f,a)) . b = f . (a,b) by Th7 .= (Proj (f,b)) . a by Th8 ; hence (Proj (f,a)) . b = (Proj (f,b)) . a ; ::_thesis: verum end; registration let S be non empty RelStr ; let T be non empty reflexive RelStr ; cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total antitone for Element of bool [: the carrier of S, the carrier of T:]; existence ex b1 being Function of S,T st b1 is antitone proof set c = the Element of T; take f = S --> the Element of T; ::_thesis: f is antitone let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) ) assume [x,y] in the InternalRel of S ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) let a, b be Element of T; ::_thesis: ( not a = f . x or not b = f . y or b <= a ) assume that A1: a = f . x and A2: b = f . y ; ::_thesis: b <= a a = the Element of T by A1, FUNCOP_1:7; hence b <= a by A2, FUNCOP_1:7; ::_thesis: verum end; end; theorem Th10: :: WAYBEL24:10 for R, S, T being non empty reflexive RelStr for f being Function of [:R,S:],T for a being Element of R for b being Element of S st f is monotone holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) proof let R, S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of [:R,S:],T for a being Element of R for b being Element of S st f is monotone holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) let f be Function of [:R,S:],T; ::_thesis: for a being Element of R for b being Element of S st f is monotone holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) let a be Element of R; ::_thesis: for b being Element of S st f is monotone holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) let b be Element of S; ::_thesis: ( f is monotone implies ( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) reconsider a = a as Element of R ; reconsider b = b as Element of S ; set g = Proj (f,b); set h = Proj (f,a); assume A1: f is monotone ; ::_thesis: ( Proj (f,a) is monotone & Proj (f,b) is monotone ) A2: now__::_thesis:_for_x,_y_being_Element_of_R_st_x_<=_y_holds_ (Proj_(f,b))_._x_<=_(Proj_(f,b))_._y let x, y be Element of R; ::_thesis: ( x <= y implies (Proj (f,b)) . x <= (Proj (f,b)) . y ) A3: b <= b ; A4: ( (Proj (f,b)) . x = f . (x,b) & (Proj (f,b)) . y = f . (y,b) ) by Th8; assume x <= y ; ::_thesis: (Proj (f,b)) . x <= (Proj (f,b)) . y then [x,b] <= [y,b] by A3, YELLOW_3:11; hence (Proj (f,b)) . x <= (Proj (f,b)) . y by A1, A4, WAYBEL_1:def_2; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_ (Proj_(f,a))_._x_<=_(Proj_(f,a))_._y let x, y be Element of S; ::_thesis: ( x <= y implies (Proj (f,a)) . x <= (Proj (f,a)) . y ) A5: a <= a ; A6: ( (Proj (f,a)) . x = f . (a,x) & (Proj (f,a)) . y = f . (a,y) ) by Th7; assume x <= y ; ::_thesis: (Proj (f,a)) . x <= (Proj (f,a)) . y then [a,x] <= [a,y] by A5, YELLOW_3:11; hence (Proj (f,a)) . x <= (Proj (f,a)) . y by A1, A6, WAYBEL_1:def_2; ::_thesis: verum end; hence ( Proj (f,a) is monotone & Proj (f,b) is monotone ) by A2, WAYBEL_1:def_2; ::_thesis: verum end; theorem Th11: :: WAYBEL24:11 for R, S, T being non empty reflexive RelStr for f being Function of [:R,S:],T for a being Element of R for b being Element of S st f is antitone holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) proof let R, S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of [:R,S:],T for a being Element of R for b being Element of S st f is antitone holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) let f be Function of [:R,S:],T; ::_thesis: for a being Element of R for b being Element of S st f is antitone holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) let a be Element of R; ::_thesis: for b being Element of S st f is antitone holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) let b be Element of S; ::_thesis: ( f is antitone implies ( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) reconsider a9 = a as Element of R ; set g = Proj (f,b); set h = Proj (f,a); assume A1: f is antitone ; ::_thesis: ( Proj (f,a) is antitone & Proj (f,b) is antitone ) A2: now__::_thesis:_for_x,_y_being_Element_of_R_st_x_<=_y_holds_ (Proj_(f,b))_._x_>=_(Proj_(f,b))_._y reconsider b9 = b as Element of S ; let x, y be Element of R; ::_thesis: ( x <= y implies (Proj (f,b)) . x >= (Proj (f,b)) . y ) A3: b9 <= b9 ; A4: ( (Proj (f,b)) . x = f . (x,b) & (Proj (f,b)) . y = f . (y,b) ) by Th8; assume x <= y ; ::_thesis: (Proj (f,b)) . x >= (Proj (f,b)) . y then [x,b9] <= [y,b9] by A3, YELLOW_3:11; hence (Proj (f,b)) . x >= (Proj (f,b)) . y by A1, A4, WAYBEL_0:def_5; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_ (Proj_(f,a))_._x_>=_(Proj_(f,a))_._y let x, y be Element of S; ::_thesis: ( x <= y implies (Proj (f,a)) . x >= (Proj (f,a)) . y ) A5: a9 <= a9 ; A6: ( (Proj (f,a)) . x = f . (a,x) & (Proj (f,a)) . y = f . (a,y) ) by Th7; assume x <= y ; ::_thesis: (Proj (f,a)) . x >= (Proj (f,a)) . y then [a9,x] <= [a9,y] by A5, YELLOW_3:11; hence (Proj (f,a)) . x >= (Proj (f,a)) . y by A1, A6, WAYBEL_0:def_5; ::_thesis: verum end; hence ( Proj (f,a) is antitone & Proj (f,b) is antitone ) by A2, WAYBEL_9:def_1; ::_thesis: verum end; registration let R, S, T be non empty reflexive RelStr ; let f be monotone Function of [:R,S:],T; let a be Element of R; cluster Proj (f,a) -> monotone ; coherence Proj (f,a) is monotone by Th10; end; registration let R, S, T be non empty reflexive RelStr ; let f be monotone Function of [:R,S:],T; let b be Element of S; cluster Proj (f,b) -> monotone ; coherence Proj (f,b) is monotone by Th10; end; registration let R, S, T be non empty reflexive RelStr ; let f be antitone Function of [:R,S:],T; let a be Element of R; cluster Proj (f,a) -> antitone ; coherence Proj (f,a) is antitone by Th11; end; registration let R, S, T be non empty reflexive RelStr ; let f be antitone Function of [:R,S:],T; let b be Element of S; cluster Proj (f,b) -> antitone ; coherence Proj (f,b) is antitone by Th11; end; theorem Th12: :: WAYBEL24:12 for R, S, T being LATTICE for f being Function of [:R,S:],T st ( for a being Element of R for b being Element of S holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds f is monotone proof let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R for b being Element of S holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds f is monotone let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R for b being Element of S holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) implies f is monotone ) assume A1: for a being Element of R for b being Element of S holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) ; ::_thesis: f is monotone now__::_thesis:_for_x,_y_being_Element_of_[:R,S:]_st_x_<=_y_holds_ f_._x_<=_f_._y let x, y be Element of [:R,S:]; ::_thesis: ( x <= y implies f . x <= f . y ) assume A2: x <= y ; ::_thesis: f . x <= f . y then A3: x `1 <= y `1 by YELLOW_3:12; A4: x `2 <= y `2 by A2, YELLOW_3:12; A5: f . ((x `1),(y `2)) = (Proj (f,(x `1))) . (y `2) by Th7; ( Proj (f,(x `1)) is monotone & f . ((x `1),(x `2)) = (Proj (f,(x `1))) . (x `2) ) by A1, Th7; then A6: f . [(x `1),(x `2)] <= f . [(x `1),(y `2)] by A4, A5, WAYBEL_1:def_2; A7: f . ((y `1),(y `2)) = (Proj (f,(y `2))) . (y `1) by Th8; ( Proj (f,(y `2)) is monotone & f . ((x `1),(y `2)) = (Proj (f,(y `2))) . (x `1) ) by A1, Th8; then f . [(x `1),(y `2)] <= f . [(y `1),(y `2)] by A3, A7, WAYBEL_1:def_2; then A8: f . [(x `1),(x `2)] <= f . [(y `1),(y `2)] by A6, YELLOW_0:def_2; A9: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2; then f . [(y `1),(y `2)] = f . y by MCART_1:21; hence f . x <= f . y by A8, A9, MCART_1:21; ::_thesis: verum end; hence f is monotone by WAYBEL_1:def_2; ::_thesis: verum end; theorem :: WAYBEL24:13 for R, S, T being LATTICE for f being Function of [:R,S:],T st ( for a being Element of R for b being Element of S holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds f is antitone proof let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R for b being Element of S holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds f is antitone let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R for b being Element of S holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) implies f is antitone ) assume A1: for a being Element of R for b being Element of S holds ( Proj (f,a) is antitone & Proj (f,b) is antitone ) ; ::_thesis: f is antitone now__::_thesis:_for_x,_y_being_Element_of_[:R,S:]_st_x_<=_y_holds_ f_._x_>=_f_._y let x, y be Element of [:R,S:]; ::_thesis: ( x <= y implies f . x >= f . y ) assume A2: x <= y ; ::_thesis: f . x >= f . y then A3: x `1 <= y `1 by YELLOW_3:12; A4: x `2 <= y `2 by A2, YELLOW_3:12; A5: f . ((x `1),(y `2)) = (Proj (f,(x `1))) . (y `2) by Th7; ( Proj (f,(x `1)) is antitone & f . ((x `1),(x `2)) = (Proj (f,(x `1))) . (x `2) ) by A1, Th7; then A6: f . [(x `1),(x `2)] >= f . [(x `1),(y `2)] by A4, A5, WAYBEL_9:def_1; A7: f . ((y `1),(y `2)) = (Proj (f,(y `2))) . (y `1) by Th8; ( Proj (f,(y `2)) is antitone & f . ((x `1),(y `2)) = (Proj (f,(y `2))) . (x `1) ) by A1, Th8; then f . [(x `1),(y `2)] >= f . [(y `1),(y `2)] by A3, A7, WAYBEL_9:def_1; then A8: f . [(x `1),(x `2)] >= f . [(y `1),(y `2)] by A6, YELLOW_0:def_2; A9: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2; then f . [(y `1),(y `2)] = f . y by MCART_1:21; hence f . x >= f . y by A8, A9, MCART_1:21; ::_thesis: verum end; hence f is antitone by WAYBEL_9:def_1; ::_thesis: verum end; theorem Th14: :: WAYBEL24:14 for R, S, T being LATTICE for f being Function of [:R,S:],T for b being Element of S for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:] proof let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T for b being Element of S for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:] let f be Function of [:R,S:],T; ::_thesis: for b being Element of S for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:] let b be Element of S; ::_thesis: for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:] let X be Subset of R; ::_thesis: (Proj (f,b)) .: X = f .: [:X,{b}:] A1: (Proj (f,b)) .: X c= f .: [:X,{b}:] proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in (Proj (f,b)) .: X or c in f .: [:X,{b}:] ) assume c in (Proj (f,b)) .: X ; ::_thesis: c in f .: [:X,{b}:] then consider k being set such that A2: k in dom (Proj (f,b)) and A3: k in X and A4: c = (Proj (f,b)) . k by FUNCT_1:def_6; b in {b} by TARSKI:def_1; then A5: [k,b] in [:X,{b}:] by A3, ZFMISC_1:87; [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2; then dom f = [: the carrier of R, the carrier of S:] by FUNCT_2:def_1; then A6: [k,b] in dom f by A2, ZFMISC_1:87; c = f . (k,b) by A2, A4, Th8; hence c in f .: [:X,{b}:] by A5, A6, FUNCT_1:def_6; ::_thesis: verum end; f .: [:X,{b}:] c= (Proj (f,b)) .: X proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in f .: [:X,{b}:] or c in (Proj (f,b)) .: X ) assume c in f .: [:X,{b}:] ; ::_thesis: c in (Proj (f,b)) .: X then consider k being set such that k in dom f and A7: k in [:X,{b}:] and A8: c = f . k by FUNCT_1:def_6; consider k1, k2 being set such that A9: k1 in X and A10: k2 in {b} and A11: k = [k1,k2] by A7, ZFMISC_1:def_2; A12: k2 = b by A10, TARSKI:def_1; c = f . (k1,k2) by A8, A11; then ( dom (Proj (f,b)) = the carrier of R & c = (Proj (f,b)) . k1 ) by A9, A12, Th8, FUNCT_2:def_1; hence c in (Proj (f,b)) .: X by A9, FUNCT_1:def_6; ::_thesis: verum end; hence (Proj (f,b)) .: X = f .: [:X,{b}:] by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th15: :: WAYBEL24:15 for R, S, T being LATTICE for f being Function of [:R,S:],T for b being Element of R for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:] proof let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T for b being Element of R for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:] let f be Function of [:R,S:],T; ::_thesis: for b being Element of R for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:] let b be Element of R; ::_thesis: for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:] let X be Subset of S; ::_thesis: (Proj (f,b)) .: X = f .: [:{b},X:] A1: (Proj (f,b)) .: X c= f .: [:{b},X:] proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in (Proj (f,b)) .: X or c in f .: [:{b},X:] ) assume c in (Proj (f,b)) .: X ; ::_thesis: c in f .: [:{b},X:] then consider k being set such that A2: k in dom (Proj (f,b)) and A3: k in X and A4: c = (Proj (f,b)) . k by FUNCT_1:def_6; b in {b} by TARSKI:def_1; then A5: [b,k] in [:{b},X:] by A3, ZFMISC_1:87; [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2; then dom f = [: the carrier of R, the carrier of S:] by FUNCT_2:def_1; then A6: [b,k] in dom f by A2, ZFMISC_1:87; c = f . (b,k) by A2, A4, Th7; hence c in f .: [:{b},X:] by A5, A6, FUNCT_1:def_6; ::_thesis: verum end; f .: [:{b},X:] c= (Proj (f,b)) .: X proof let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in f .: [:{b},X:] or c in (Proj (f,b)) .: X ) assume c in f .: [:{b},X:] ; ::_thesis: c in (Proj (f,b)) .: X then consider k being set such that k in dom f and A7: k in [:{b},X:] and A8: c = f . k by FUNCT_1:def_6; consider k1, k2 being set such that A9: k1 in {b} and A10: k2 in X and A11: k = [k1,k2] by A7, ZFMISC_1:def_2; A12: k1 = b by A9, TARSKI:def_1; c = f . (k1,k2) by A8, A11; then ( dom (Proj (f,b)) = the carrier of S & c = (Proj (f,b)) . k2 ) by A10, A12, Th7, FUNCT_2:def_1; hence c in (Proj (f,b)) .: X by A10, FUNCT_1:def_6; ::_thesis: verum end; hence (Proj (f,b)) .: X = f .: [:{b},X:] by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: WAYBEL24:16 for R, S, T being LATTICE for f being Function of [:R,S:],T for a being Element of R for b being Element of S st f is directed-sups-preserving holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) proof let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T for a being Element of R for b being Element of S st f is directed-sups-preserving holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) let f be Function of [:R,S:],T; ::_thesis: for a being Element of R for b being Element of S st f is directed-sups-preserving holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) let a be Element of R; ::_thesis: for b being Element of S st f is directed-sups-preserving holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) let b be Element of S; ::_thesis: ( f is directed-sups-preserving implies ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) assume A1: f is directed-sups-preserving ; ::_thesis: ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) A2: for X being Subset of S st not X is empty & X is directed holds Proj (f,a) preserves_sup_of X proof reconsider Y9 = {a} as non empty directed Subset of R by WAYBEL_0:5; let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies Proj (f,a) preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: Proj (f,a) preserves_sup_of X then reconsider X9 = X as non empty directed Subset of S ; Proj (f,a) preserves_sup_of X proof A3: sup Y9 = a by YELLOW_0:39; A4: f preserves_sup_of [:Y9,X9:] by A1, WAYBEL_0:def_37; A5: (Proj (f,a)) .: X = f .: [:Y9,X9:] by Th15; A6: ex_sup_of Y9,R by YELLOW_0:38; assume A7: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) ) then A8: ex_sup_of [:Y9,X9:],[:R,S:] by A6, YELLOW_3:39; sup ((Proj (f,a)) .: X) = sup (f .: [:Y9,X9:]) by Th15 .= f . (sup [:Y9,X9:]) by A8, A4, WAYBEL_0:def_31 .= f . ((sup Y9),(sup X9)) by A7, A6, YELLOW_3:43 .= (Proj (f,a)) . (sup X) by A3, Th7 ; hence ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) ) by A8, A4, A5, WAYBEL_0:def_31; ::_thesis: verum end; hence Proj (f,a) preserves_sup_of X ; ::_thesis: verum end; for X being Subset of R st not X is empty & X is directed holds Proj (f,b) preserves_sup_of X proof reconsider Y9 = {b} as non empty directed Subset of S by WAYBEL_0:5; let X be Subset of R; ::_thesis: ( not X is empty & X is directed implies Proj (f,b) preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: Proj (f,b) preserves_sup_of X then reconsider X9 = X as non empty directed Subset of R ; Proj (f,b) preserves_sup_of X proof A9: sup Y9 = b by YELLOW_0:39; A10: f preserves_sup_of [:X9,Y9:] by A1, WAYBEL_0:def_37; A11: (Proj (f,b)) .: X = f .: [:X9,Y9:] by Th14; A12: ex_sup_of Y9,S by YELLOW_0:38; assume A13: ex_sup_of X,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) ) then A14: ex_sup_of [:X9,Y9:],[:R,S:] by A12, YELLOW_3:39; sup ((Proj (f,b)) .: X) = sup (f .: [:X9,Y9:]) by Th14 .= f . (sup [:X9,Y9:]) by A14, A10, WAYBEL_0:def_31 .= f . ((sup X9),(sup Y9)) by A13, A12, YELLOW_3:43 .= (Proj (f,b)) . (sup X) by A9, Th8 ; hence ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) ) by A14, A10, A11, WAYBEL_0:def_31; ::_thesis: verum end; hence Proj (f,b) preserves_sup_of X ; ::_thesis: verum end; hence ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) by A2, WAYBEL_0:def_37; ::_thesis: verum end; theorem Th17: :: WAYBEL24:17 for R, S, T being LATTICE for f being monotone Function of [:R,S:],T for a being Element of R for b being Element of S for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds f . [a,b] <= sup (f .: X) proof let R, S, T be LATTICE; ::_thesis: for f being monotone Function of [:R,S:],T for a being Element of R for b being Element of S for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds f . [a,b] <= sup (f .: X) let f be monotone Function of [:R,S:],T; ::_thesis: for a being Element of R for b being Element of S for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds f . [a,b] <= sup (f .: X) let a be Element of R; ::_thesis: for b being Element of S for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds f . [a,b] <= sup (f .: X) let b be Element of S; ::_thesis: for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds f . [a,b] <= sup (f .: X) let X be directed Subset of [:R,S:]; ::_thesis: ( ex_sup_of f .: X,T & a in proj1 X & b in proj2 X implies f . [a,b] <= sup (f .: X) ) assume that A1: ex_sup_of f .: X,T and A2: a in proj1 X and A3: b in proj2 X ; ::_thesis: f . [a,b] <= sup (f .: X) consider d being set such that A4: [d,b] in X by A3, XTUPLE_0:def_13; d in proj1 X by A4, XTUPLE_0:def_12; then reconsider d = d as Element of R ; consider c being set such that A5: [a,c] in X by A2, XTUPLE_0:def_12; c in proj2 X by A5, XTUPLE_0:def_13; then reconsider c = c as Element of S ; consider z being Element of [:R,S:] such that A6: z in X and A7: ( [a,c] <= z & [d,b] <= z ) by A5, A4, WAYBEL_0:def_1; A8: f .: X is_<=_than sup (f .: X) by A1, YELLOW_0:30; [a,c] "\/" [d,b] <= z "\/" z by A7, YELLOW_3:3; then [a,c] "\/" [d,b] <= z by YELLOW_5:1; then [(a "\/" d),(c "\/" b)] <= z by YELLOW10:16; then A9: f . [(a "\/" d),(c "\/" b)] <= f . z by WAYBEL_1:def_2; dom f = the carrier of [:R,S:] by FUNCT_2:def_1; then f . z in f .: X by A6, FUNCT_1:def_6; then A10: f . z <= sup (f .: X) by A8, LATTICE3:def_9; ( a <= a "\/" d & b <= c "\/" b ) by YELLOW_0:22; then [a,b] <= [(a "\/" d),(c "\/" b)] by YELLOW_3:11; then f . [a,b] <= f . [(a "\/" d),(c "\/" b)] by WAYBEL_1:def_2; then f . [a,b] <= f . z by A9, YELLOW_0:def_2; hence f . [a,b] <= sup (f .: X) by A10, YELLOW_0:def_2; ::_thesis: verum end; theorem :: WAYBEL24:18 for R, S, T being complete LATTICE for f being Function of [:R,S:],T st ( for a being Element of R for b being Element of S holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds f is directed-sups-preserving proof let R, S, T be complete LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R for b being Element of S holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds f is directed-sups-preserving let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R for b being Element of S holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) implies f is directed-sups-preserving ) assume A1: for a being Element of R for b being Element of S holds ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ; ::_thesis: f is directed-sups-preserving for X being Subset of [:R,S:] st not X is empty & X is directed holds f preserves_sup_of X proof let X be Subset of [:R,S:]; ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: f preserves_sup_of X then reconsider X = X as non empty directed Subset of [:R,S:] ; for a being Element of R for b being Element of S holds ( Proj (f,a) is monotone & Proj (f,b) is monotone ) by A1, WAYBEL17:3; then A2: f is monotone by Th12; f preserves_sup_of X proof ( proj1 X is directed & not proj1 X is empty & Proj (f,("\/" ((proj2 X),S))) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22; then A3: Proj (f,("\/" ((proj2 X),S))) preserves_sup_of proj1 X by WAYBEL_0:def_37; A4: ex_sup_of (Proj (f,(sup (proj2 X)))) .: (proj1 X),T by YELLOW_0:17; assume A5: ex_sup_of X,[:R,S:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) ) then A6: ex_sup_of proj1 X,R by YELLOW_3:41; A7: ex_sup_of proj2 X,S by A5, YELLOW_3:41; for b being Element of T st b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) holds b <= sup (f .: X) proof let b be Element of T; ::_thesis: ( b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) implies b <= sup (f .: X) ) assume b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) ; ::_thesis: b <= sup (f .: X) then consider b1 being set such that A8: b1 in dom (Proj (f,(sup (proj2 X)))) and A9: b1 in proj1 X and A10: b = (Proj (f,(sup (proj2 X)))) . b1 by FUNCT_1:def_6; reconsider b1 = b1 as Element of R by A8; A11: (Proj (f,b1)) .: (proj2 X) is_<=_than sup (f .: X) proof let k be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not k in (Proj (f,b1)) .: (proj2 X) or k <= sup (f .: X) ) assume k in (Proj (f,b1)) .: (proj2 X) ; ::_thesis: k <= sup (f .: X) then consider k1 being set such that A12: k1 in dom (Proj (f,b1)) and A13: k1 in proj2 X and A14: k = (Proj (f,b1)) . k1 by FUNCT_1:def_6; reconsider k1 = k1 as Element of S by A12; k = f . (b1,k1) by A14, Th7; hence k <= sup (f .: X) by A2, A9, A13, Th17, YELLOW_0:17; ::_thesis: verum end; ( not proj2 X is empty & proj2 X is directed & Proj (f,b1) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22; then A15: Proj (f,b1) preserves_sup_of proj2 X by WAYBEL_0:def_37; A16: ex_sup_of (Proj (f,b1)) .: (proj2 X),T by YELLOW_0:17; b = (Proj (f,b1)) . (sup (proj2 X)) by A10, Th9 .= sup ((Proj (f,b1)) .: (proj2 X)) by A7, A15, WAYBEL_0:def_31 ; hence b <= sup (f .: X) by A16, A11, YELLOW_0:def_9; ::_thesis: verum end; then A17: (Proj (f,(sup (proj2 X)))) .: (proj1 X) is_<=_than sup (f .: X) by LATTICE3:def_9; A18: sup (f .: X) <= f . (sup X) by A2, WAYBEL17:16; f . (sup X) = f . ((sup (proj1 X)),(sup (proj2 X))) by YELLOW_3:46 .= (Proj (f,(sup (proj2 X)))) . (sup (proj1 X)) by Th8 .= sup ((Proj (f,(sup (proj2 X)))) .: (proj1 X)) by A6, A3, WAYBEL_0:def_31 ; then f . (sup X) <= sup (f .: X) by A17, A4, YELLOW_0:def_9; hence ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) ) by A18, YELLOW_0:17, YELLOW_0:def_3; ::_thesis: verum end; hence f preserves_sup_of X ; ::_thesis: verum end; hence f is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum end; theorem Th19: :: WAYBEL24:19 for S being set for T being non empty RelStr for f being set holds ( f is Element of (T |^ S) iff f is Function of S, the carrier of T ) proof let S be set ; ::_thesis: for T being non empty RelStr for f being set holds ( f is Element of (T |^ S) iff f is Function of S, the carrier of T ) let T be non empty RelStr ; ::_thesis: for f being set holds ( f is Element of (T |^ S) iff f is Function of S, the carrier of T ) let f be set ; ::_thesis: ( f is Element of (T |^ S) iff f is Function of S, the carrier of T ) hereby ::_thesis: ( f is Function of S, the carrier of T implies f is Element of (T |^ S) ) assume f is Element of (T |^ S) ; ::_thesis: f is Function of S, the carrier of T then f in the carrier of (T |^ S) ; then f in Funcs (S, the carrier of T) by YELLOW_1:28; then ex a being Function st ( a = f & dom a = S & rng a c= the carrier of T ) by FUNCT_2:def_2; hence f is Function of S, the carrier of T by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; assume f is Function of S, the carrier of T ; ::_thesis: f is Element of (T |^ S) then f in Funcs (S, the carrier of T) by FUNCT_2:8; hence f is Element of (T |^ S) by YELLOW_1:28; ::_thesis: verum end; begin definition let S be TopStruct ; let T be non empty TopRelStr ; func ContMaps (S,T) -> strict RelStr means :Def3: :: WAYBEL24:def 3 ( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of it iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) ); existence ex b1 being strict RelStr st ( b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of b1 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) ) proof defpred S1[ set ] means ex f being Function of S,T st ( \$1 = f & f is continuous ); consider X being set such that A1: for a being set holds ( a in X iff ( a in the carrier of (T |^ the carrier of S) & S1[a] ) ) from XBOOLE_0:sch_1(); X c= the carrier of (T |^ the carrier of S) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in the carrier of (T |^ the carrier of S) ) assume a in X ; ::_thesis: a in the carrier of (T |^ the carrier of S) hence a in the carrier of (T |^ the carrier of S) by A1; ::_thesis: verum end; then reconsider X = X as Subset of (T |^ the carrier of S) ; take SX = subrelstr X; ::_thesis: ( SX is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of SX iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) ) thus SX is full SubRelStr of T |^ the carrier of S ; ::_thesis: for x being set holds ( x in the carrier of SX iff ex f being Function of S,T st ( x = f & f is continuous ) ) let f be set ; ::_thesis: ( f in the carrier of SX iff ex f being Function of S,T st ( f = f & f is continuous ) ) hereby ::_thesis: ( ex f being Function of S,T st ( f = f & f is continuous ) implies f in the carrier of SX ) assume f in the carrier of SX ; ::_thesis: ex f9 being Function of S,T st ( f9 = f & f9 is continuous ) then f in X by YELLOW_0:def_15; then consider f9 being Function of S,T such that A2: ( f9 = f & f9 is continuous ) by A1; take f9 = f9; ::_thesis: ( f9 = f & f9 is continuous ) thus ( f9 = f & f9 is continuous ) by A2; ::_thesis: verum end; given f9 being Function of S,T such that A3: f = f9 and A4: f9 is continuous ; ::_thesis: f in the carrier of SX f in Funcs ( the carrier of S, the carrier of T) by A3, FUNCT_2:8; then f in the carrier of (T |^ the carrier of S) by YELLOW_1:28; then f in X by A1, A3, A4; hence f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum end; uniqueness for b1, b2 being strict RelStr st b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of b1 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) & b2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of b2 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) holds b1 = b2 proof let A1, A2 be strict RelStr ; ::_thesis: ( A1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of A1 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) & A2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of A2 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) implies A1 = A2 ) assume that A5: A1 is full SubRelStr of T |^ the carrier of S and A6: for x being set holds ( x in the carrier of A1 iff ex f being Function of S,T st ( x = f & f is continuous ) ) and A7: A2 is full SubRelStr of T |^ the carrier of S and A8: for x being set holds ( x in the carrier of A2 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ; ::_thesis: A1 = A2 the carrier of A1 = the carrier of A2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of A2 c= the carrier of A1 let x be set ; ::_thesis: ( x in the carrier of A1 implies x in the carrier of A2 ) assume x in the carrier of A1 ; ::_thesis: x in the carrier of A2 then ex f being Function of S,T st ( x = f & f is continuous ) by A6; hence x in the carrier of A2 by A8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A2 or x in the carrier of A1 ) assume x in the carrier of A2 ; ::_thesis: x in the carrier of A1 then ex f being Function of S,T st ( x = f & f is continuous ) by A8; hence x in the carrier of A1 by A6; ::_thesis: verum end; hence A1 = A2 by A5, A7, YELLOW_0:57; ::_thesis: verum end; end; :: deftheorem Def3 defines ContMaps WAYBEL24:def_3_:_ for S being TopStruct for T being non empty TopRelStr for b3 being strict RelStr holds ( b3 = ContMaps (S,T) iff ( b3 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of b3 iff ex f being Function of S,T st ( x = f & f is continuous ) ) ) ) ); registration let S be non empty TopSpace; let T be non empty TopSpace-like TopRelStr ; cluster ContMaps (S,T) -> non empty strict ; coherence not ContMaps (S,T) is empty proof set f = the continuous Function of S,T; the continuous Function of S,T in the carrier of (ContMaps (S,T)) by Def3; hence not ContMaps (S,T) is empty ; ::_thesis: verum end; end; registration let S be non empty TopSpace; let T be non empty TopSpace-like TopRelStr ; cluster ContMaps (S,T) -> constituted-Functions strict ; coherence ContMaps (S,T) is constituted-Functions proof let a be Element of (ContMaps (S,T)); :: according to MONOID_0:def_1 ::_thesis: a is set ex a9 being Function of S,T st ( a9 = a & a9 is continuous ) by Def3; hence a is set ; ::_thesis: verum end; end; theorem Th20: :: WAYBEL24:20 for S being non empty TopSpace for T being non empty TopSpace-like reflexive TopRelStr for x, y being Element of (ContMaps (S,T)) holds ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) proof let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like reflexive TopRelStr for x, y being Element of (ContMaps (S,T)) holds ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) let T be non empty TopSpace-like reflexive TopRelStr ; ::_thesis: for x, y being Element of (ContMaps (S,T)) holds ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) let x, y be Element of (ContMaps (S,T)); ::_thesis: ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) A1: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3; then reconsider x9 = x, y9 = y as Element of (T |^ the carrier of S) by YELLOW_0:58; reconsider xa = x9, ya = y9 as Function of S,T by Th19; hereby ::_thesis: ( ( for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) implies x <= y ) assume A2: x <= y ; ::_thesis: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T let i be Element of S; ::_thesis: [(x . i),(y . i)] in the InternalRel of T x9 <= y9 by A1, A2, YELLOW_0:59; then xa <= ya by WAYBEL10:11; then ex a, b being Element of T st ( a = xa . i & b = ya . i & a <= b ) by YELLOW_2:def_1; hence [(x . i),(y . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum end; assume A3: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ; ::_thesis: x <= y now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_S_holds_ ex_a,_b_being_Element_of_T_st_ (_a_=_xa_._j_&_b_=_ya_._j_&_a_<=_b_) let j be set ; ::_thesis: ( j in the carrier of S implies ex a, b being Element of T st ( a = xa . j & b = ya . j & a <= b ) ) assume j in the carrier of S ; ::_thesis: ex a, b being Element of T st ( a = xa . j & b = ya . j & a <= b ) then reconsider i = j as Element of S ; reconsider a = xa . i, b = ya . i as Element of T ; take a = a; ::_thesis: ex b being Element of T st ( a = xa . j & b = ya . j & a <= b ) take b = b; ::_thesis: ( a = xa . j & b = ya . j & a <= b ) thus ( a = xa . j & b = ya . j ) ; ::_thesis: a <= b [a,b] in the InternalRel of T by A3; hence a <= b by ORDERS_2:def_5; ::_thesis: verum end; then xa <= ya by YELLOW_2:def_1; then x9 <= y9 by WAYBEL10:11; hence x <= y by A1, YELLOW_0:60; ::_thesis: verum end; theorem Th21: :: WAYBEL24:21 for S being non empty TopSpace for T being non empty TopSpace-like reflexive TopRelStr for x being set holds ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) ) proof let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like reflexive TopRelStr for x being set holds ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) ) let T be non empty TopSpace-like reflexive TopRelStr ; ::_thesis: for x being set holds ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) ) let x be set ; ::_thesis: ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) ) thus ( x is continuous Function of S,T implies x is Element of (ContMaps (S,T)) ) by Def3; ::_thesis: ( x is Element of (ContMaps (S,T)) implies x is continuous Function of S,T ) assume x is Element of (ContMaps (S,T)) ; ::_thesis: x is continuous Function of S,T then ex f being Function of S,T st ( x = f & f is continuous ) by Def3; hence x is continuous Function of S,T ; ::_thesis: verum end; registration let S be non empty TopSpace; let T be non empty TopSpace-like reflexive TopRelStr ; cluster ContMaps (S,T) -> strict reflexive ; coherence ContMaps (S,T) is reflexive proof reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3; CS is reflexive ; hence ContMaps (S,T) is reflexive ; ::_thesis: verum end; end; registration let S be non empty TopSpace; let T be non empty TopSpace-like transitive TopRelStr ; cluster ContMaps (S,T) -> strict transitive ; coherence ContMaps (S,T) is transitive proof reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3; CS is transitive ; hence ContMaps (S,T) is transitive ; ::_thesis: verum end; end; registration let S be non empty TopSpace; let T be non empty TopSpace-like antisymmetric TopRelStr ; cluster ContMaps (S,T) -> strict antisymmetric ; coherence ContMaps (S,T) is antisymmetric proof reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3; CS is antisymmetric ; hence ContMaps (S,T) is antisymmetric ; ::_thesis: verum end; end; registration let S be set ; let T be non empty RelStr ; clusterT |^ S -> constituted-Functions ; coherence T |^ S is constituted-Functions proof let a be Element of (T |^ S); :: according to MONOID_0:def_1 ::_thesis: a is set thus a is set by Th19; ::_thesis: verum end; end; theorem :: WAYBEL24:22 for S being non empty 1-sorted for T being complete LATTICE for f, g, h being Function of S,T for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds h . i = sup {(f . i),(g . i)} proof let S be non empty 1-sorted ; ::_thesis: for T being complete LATTICE for f, g, h being Function of S,T for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds h . i = sup {(f . i),(g . i)} let T be complete LATTICE; ::_thesis: for f, g, h being Function of S,T for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds h . i = sup {(f . i),(g . i)} let f, g, h be Function of S,T; ::_thesis: for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds h . i = sup {(f . i),(g . i)} let i be Element of S; ::_thesis: ( h = "\/" ({f,g},(T |^ the carrier of S)) implies h . i = sup {(f . i),(g . i)} ) reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19; reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ; reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ; A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7; reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def_5; reconsider DU = {f9,g9} as Subset of (product SYT) ; assume h = "\/" ({f,g},(T |^ the carrier of S)) ; ::_thesis: h . i = sup {(f . i),(g . i)} then h . i = (sup DU) . i by YELLOW_1:def_5 .= "\/" ((pi ({f,g},i)),(SYT . i)) by A1, WAYBEL_3:32 .= "\/" ((pi ({f,g},i)),T) by FUNCOP_1:7 .= sup {(f . i),(g . i)} by CARD_3:15 ; hence h . i = sup {(f . i),(g . i)} ; ::_thesis: verum end; theorem Th23: :: WAYBEL24:23 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds for X being Subset of (product J) for i being Element of I holds (inf X) . i = inf (pi (X,i)) proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds for X being Subset of (product J) for i being Element of I holds (inf X) . i = inf (pi (X,i)) let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for X being Subset of (product J) for i being Element of I holds (inf X) . i = inf (pi (X,i)) ) assume A1: for i being Element of I holds J . i is complete LATTICE ; ::_thesis: for X being Subset of (product J) for i being Element of I holds (inf X) . i = inf (pi (X,i)) then reconsider L = product J as complete LATTICE by WAYBEL_3:31; let X be Subset of (product J); ::_thesis: for i being Element of I holds (inf X) . i = inf (pi (X,i)) let i be Element of I; ::_thesis: (inf X) . i = inf (pi (X,i)) A2: L is complete ; then A3: inf X is_<=_than X by YELLOW_0:33; A4: (inf X) . i is_<=_than pi (X,i) proof let a be Element of (J . i); :: according to LATTICE3:def_8 ::_thesis: ( not a in pi (X,i) or (inf X) . i <= a ) assume a in pi (X,i) ; ::_thesis: (inf X) . i <= a then consider f being Function such that A5: f in X and A6: a = f . i by CARD_3:def_6; reconsider f = f as Element of (product J) by A5; inf X <= f by A3, A5, LATTICE3:def_8; hence (inf X) . i <= a by A6, WAYBEL_3:28; ::_thesis: verum end; A7: now__::_thesis:_for_a_being_Element_of_(J_._i)_st_a_is_<=_than_pi_(X,i)_holds_ (inf_X)_._i_>=_a let a be Element of (J . i); ::_thesis: ( a is_<=_than pi (X,i) implies (inf X) . i >= a ) set f = (inf X) +* (i,a); A8: dom ((inf X) +* (i,a)) = dom (inf X) by FUNCT_7:30; A9: dom (inf X) = I by WAYBEL_3:27; now__::_thesis:_for_j_being_Element_of_I_holds_((inf_X)_+*_(i,a))_._j_is_Element_of_(J_._j) let j be Element of I; ::_thesis: ((inf X) +* (i,a)) . j is Element of (J . j) ( j = i or j <> i ) ; then ( ((inf X) +* (i,a)) . j = (inf X) . j or ( ((inf X) +* (i,a)) . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32; hence ((inf X) +* (i,a)) . j is Element of (J . j) ; ::_thesis: verum end; then reconsider f = (inf X) +* (i,a) as Element of (product J) by A8, WAYBEL_3:27; assume A10: a is_<=_than pi (X,i) ; ::_thesis: (inf X) . i >= a f is_<=_than X proof let g be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not g in X or f <= g ) assume g in X ; ::_thesis: f <= g then A11: ( g >= inf X & g . i in pi (X,i) ) by A2, CARD_3:def_6, YELLOW_2:22; now__::_thesis:_for_j_being_Element_of_I_holds_f_._j_<=_g_._j let j be Element of I; ::_thesis: f . j <= g . j ( j = i or j <> i ) ; then ( f . j = (inf X) . j or ( f . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32; hence f . j <= g . j by A10, A11, LATTICE3:def_8, WAYBEL_3:28; ::_thesis: verum end; hence f <= g by WAYBEL_3:28; ::_thesis: verum end; then A12: f <= inf X by A2, YELLOW_0:33; f . i = a by A9, FUNCT_7:31; hence (inf X) . i >= a by A12, WAYBEL_3:28; ::_thesis: verum end; J . i is complete LATTICE by A1; hence (inf X) . i = inf (pi (X,i)) by A4, A7, YELLOW_0:33; ::_thesis: verum end; theorem :: WAYBEL24:24 for S being non empty 1-sorted for T being complete LATTICE for f, g, h being Function of S,T for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds h . i = inf {(f . i),(g . i)} proof let S be non empty 1-sorted ; ::_thesis: for T being complete LATTICE for f, g, h being Function of S,T for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds h . i = inf {(f . i),(g . i)} let T be complete LATTICE; ::_thesis: for f, g, h being Function of S,T for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds h . i = inf {(f . i),(g . i)} let f, g, h be Function of S,T; ::_thesis: for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds h . i = inf {(f . i),(g . i)} let i be Element of S; ::_thesis: ( h = "/\" ({f,g},(T |^ the carrier of S)) implies h . i = inf {(f . i),(g . i)} ) reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19; reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ; reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ; A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7; reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def_5; reconsider DU = {f9,g9} as Subset of (product SYT) ; assume h = "/\" ({f,g},(T |^ the carrier of S)) ; ::_thesis: h . i = inf {(f . i),(g . i)} then h . i = (inf DU) . i by YELLOW_1:def_5 .= "/\" ((pi ({f,g},i)),(SYT . i)) by A1, Th23 .= "/\" ((pi ({f,g},i)),T) by FUNCOP_1:7 .= inf {(f . i),(g . i)} by CARD_3:15 ; hence h . i = inf {(f . i),(g . i)} ; ::_thesis: verum end; theorem Th25: :: WAYBEL24:25 for S being non empty RelStr for T being complete LATTICE for F being non empty Subset of (T |^ the carrier of S) for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) proof let S be non empty RelStr ; ::_thesis: for T being complete LATTICE for F being non empty Subset of (T |^ the carrier of S) for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) let T be complete LATTICE; ::_thesis: for F being non empty Subset of (T |^ the carrier of S) for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) let F be non empty Subset of (T |^ the carrier of S); ::_thesis: for i being Element of S holds (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) let i be Element of S; ::_thesis: (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ; reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ; reconsider X = F as Subset of (product SYT) by YELLOW_1:def_5; A1: pi (X,i) = { (f . i) where f is Element of (T |^ the carrier of S) : f in F } proof thus pi (X,i) c= { (f . i) where f is Element of (T |^ the carrier of S) : f in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (X,i) or a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ) assume a in pi (X,i) ; ::_thesis: a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } then ex g being Function st ( g in X & a = g . i ) by CARD_3:def_6; hence a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; ::_thesis: verum end; thus { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } or a in pi (X,i) ) assume a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; ::_thesis: a in pi (X,i) then ex g being Element of (T |^ the carrier of S) st ( a = g . i & g in F ) ; hence a in pi (X,i) by CARD_3:def_6; ::_thesis: verum end; end; ( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def_5; then (sup F) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32 .= "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A1, FUNCOP_1:7 ; hence (sup F) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) ; ::_thesis: verum end; theorem Th26: :: WAYBEL24:26 for S, T being complete TopLattice for F being non empty Subset of (ContMaps (S,T)) for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) proof let S, T be complete TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) let i be Element of S; ::_thesis: ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ; reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ; ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3; then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13; then A1: F c= the carrier of (T |^ the carrier of S) by XBOOLE_1:1; then reconsider X = F as Subset of (product SYT) by YELLOW_1:def_5; A2: pi (X,i) = { (f . i) where f is Element of (T |^ the carrier of S) : f in F } proof thus pi (X,i) c= { (f . i) where f is Element of (T |^ the carrier of S) : f in F } :: according to XBOOLE_0:def_10 ::_thesis: { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (X,i) or a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ) assume a in pi (X,i) ; ::_thesis: a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } then ex g being Function st ( g in X & a = g . i ) by CARD_3:def_6; hence a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } by A1; ::_thesis: verum end; thus { (f . i) where f is Element of (T |^ the carrier of S) : f in F } c= pi (X,i) ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } or a in pi (X,i) ) assume a in { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ; ::_thesis: a in pi (X,i) then ex g being Element of (T |^ the carrier of S) st ( a = g . i & g in F ) ; hence a in pi (X,i) by CARD_3:def_6; ::_thesis: verum end; end; ( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def_5; then ("\/" (F,(T |^ the carrier of S))) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32 .= "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, FUNCOP_1:7 ; hence ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T) ; ::_thesis: verum end; theorem Th27: :: WAYBEL24:27 for S being non empty RelStr for T being complete LATTICE for F being non empty Subset of (T |^ the carrier of S) for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } proof let S be non empty RelStr ; ::_thesis: for T being complete LATTICE for F being non empty Subset of (T |^ the carrier of S) for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } let T be complete LATTICE; ::_thesis: for F being non empty Subset of (T |^ the carrier of S) for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } let F be non empty Subset of (T |^ the carrier of S); ::_thesis: for D being non empty Subset of S holds (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } let D be non empty Subset of S; ::_thesis: (sup F) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } thus (sup F) .: D c= { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= (sup F) .: D proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (sup F) .: D or a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } ) assume a in (sup F) .: D ; ::_thesis: a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } then consider x being set such that x in dom (sup F) and A1: x in D and A2: a = (sup F) . x by FUNCT_1:def_6; reconsider x9 = x as Element of S by A1; a = "\/" ( { (f . x9) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, Th25; hence a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } by A1; ::_thesis: verum end; thus { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= (sup F) .: D ::_thesis: verum proof sup F is Function of S,T by Th6; then A3: dom (sup F) = the carrier of S by FUNCT_2:def_1; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } or a in (sup F) .: D ) assume a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } ; ::_thesis: a in (sup F) .: D then consider i1 being Element of S such that A4: ( a = "\/" ( { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T) & i1 in D ) ; a = (sup F) . i1 by A4, Th25; hence a in (sup F) .: D by A4, A3, FUNCT_1:def_6; ::_thesis: verum end; end; theorem Th28: :: WAYBEL24:28 for S, T being complete Scott TopLattice for F being non empty Subset of (ContMaps (S,T)) for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } proof let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } let D be non empty Subset of S; ::_thesis: ("\/" (F,(T |^ the carrier of S))) .: D = { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } thus ("\/" (F,(T |^ the carrier of S))) .: D c= { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= ("\/" (F,(T |^ the carrier of S))) .: D proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ("\/" (F,(T |^ the carrier of S))) .: D or a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } ) assume a in ("\/" (F,(T |^ the carrier of S))) .: D ; ::_thesis: a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } then consider x being set such that x in dom ("\/" (F,(T |^ the carrier of S))) and A1: x in D and A2: a = ("\/" (F,(T |^ the carrier of S))) . x by FUNCT_1:def_6; reconsider x9 = x as Element of S by A1; a = "\/" ( { (f . x9) where f is Element of (T |^ the carrier of S) : f in F } ,T) by A2, Th26; hence a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } by A1; ::_thesis: verum end; thus { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } c= ("\/" (F,(T |^ the carrier of S))) .: D ::_thesis: verum proof "\/" (F,(T |^ the carrier of S)) is Function of S,T by Th19; then A3: dom ("\/" (F,(T |^ the carrier of S))) = the carrier of S by FUNCT_2:def_1; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } or a in ("\/" (F,(T |^ the carrier of S))) .: D ) assume a in { ("\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)) where i is Element of S : i in D } ; ::_thesis: a in ("\/" (F,(T |^ the carrier of S))) .: D then consider i1 being Element of S such that A4: ( a = "\/" ( { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T) & i1 in D ) ; a = ("\/" (F,(T |^ the carrier of S))) . i1 by A4, Th26; hence a in ("\/" (F,(T |^ the carrier of S))) .: D by A4, A3, FUNCT_1:def_6; ::_thesis: verum end; end; scheme :: WAYBEL24:sch 3 FraenkelF9RS{ F1() -> non empty TopRelStr , F2( set ) -> set , F3( set ) -> set , P1[ set ] } : { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } provided A1: for v being Element of F1() st P1[v] holds F2(v) = F3(v) proof set X = { F2(v1) where v1 is Element of F1() : P1[v1] } ; set Y = { F3(v2) where v2 is Element of F1() : P1[v2] } ; A2: { F3(v2) where v2 is Element of F1() : P1[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(v2) where v2 is Element of F1() : P1[v2] } or x in { F2(v1) where v1 is Element of F1() : P1[v1] } ) assume x in { F3(v2) where v2 is Element of F1() : P1[v2] } ; ::_thesis: x in { F2(v1) where v1 is Element of F1() : P1[v1] } then consider v1 being Element of F1() such that A3: x = F3(v1) and A4: P1[v1] ; x = F2(v1) by A1, A3, A4; hence x in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; ::_thesis: verum end; { F2(v1) where v1 is Element of F1() : P1[v1] } c= { F3(v2) where v2 is Element of F1() : P1[v2] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F2(v1) where v1 is Element of F1() : P1[v1] } or x in { F3(v2) where v2 is Element of F1() : P1[v2] } ) assume x in { F2(v1) where v1 is Element of F1() : P1[v1] } ; ::_thesis: x in { F3(v2) where v2 is Element of F1() : P1[v2] } then consider v1 being Element of F1() such that A5: x = F2(v1) and A6: P1[v1] ; x = F3(v1) by A1, A5, A6; hence x in { F3(v2) where v2 is Element of F1() : P1[v2] } by A6; ::_thesis: verum end; hence { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } by A2, XBOOLE_0:def_10; ::_thesis: verum end; scheme :: WAYBEL24:sch 4 FraenkelF9RSS{ F1() -> non empty RelStr , F2( set ) -> set , F3( set ) -> set , P1[ set ] } : { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } provided A1: for v being Element of F1() st P1[v] holds F2(v) = F3(v) proof set X = { F2(v1) where v1 is Element of F1() : P1[v1] } ; set Y = { F3(v2) where v2 is Element of F1() : P1[v2] } ; A2: { F3(v2) where v2 is Element of F1() : P1[v2] } c= { F2(v1) where v1 is Element of F1() : P1[v1] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(v2) where v2 is Element of F1() : P1[v2] } or x in { F2(v1) where v1 is Element of F1() : P1[v1] } ) assume x in { F3(v2) where v2 is Element of F1() : P1[v2] } ; ::_thesis: x in { F2(v1) where v1 is Element of F1() : P1[v1] } then consider v1 being Element of F1() such that A3: x = F3(v1) and A4: P1[v1] ; x = F2(v1) by A1, A3, A4; hence x in { F2(v1) where v1 is Element of F1() : P1[v1] } by A4; ::_thesis: verum end; { F2(v1) where v1 is Element of F1() : P1[v1] } c= { F3(v2) where v2 is Element of F1() : P1[v2] } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F2(v1) where v1 is Element of F1() : P1[v1] } or x in { F3(v2) where v2 is Element of F1() : P1[v2] } ) assume x in { F2(v1) where v1 is Element of F1() : P1[v1] } ; ::_thesis: x in { F3(v2) where v2 is Element of F1() : P1[v2] } then consider v1 being Element of F1() such that A5: x = F2(v1) and A6: P1[v1] ; x = F3(v1) by A1, A5, A6; hence x in { F3(v2) where v2 is Element of F1() : P1[v2] } by A6; ::_thesis: verum end; hence { F2(v1) where v1 is Element of F1() : P1[v1] } = { F3(v2) where v2 is Element of F1() : P1[v2] } by A2, XBOOLE_0:def_10; ::_thesis: verum end; scheme :: WAYBEL24:sch 5 FuncFraenkelS{ F1() -> non empty TopRelStr , F2() -> non empty TopRelStr , F3( set ) -> Element of F2(), F4() -> Function, P1[ set ] } : F4() .: { F3(x) where x is Element of F1() : P1[x] } = { (F4() . F3(x)) where x is Element of F1() : P1[x] } provided A1: the carrier of F2() c= dom F4() proof set f = F4(); thus F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def_10 ::_thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ) assume y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ; ::_thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } then consider z being set such that z in dom F4() and A2: z in { F3(x) where x is Element of F1() : P1[x] } and A3: y = F4() . z by FUNCT_1:def_6; ex x being Element of F1() st ( z = F3(x) & P1[x] ) by A2; hence y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } by A3; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ) assume y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ; ::_thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] } then consider x being Element of F1() such that A4: y = F4() . F3(x) and A5: P1[x] ; ( F3(x) in the carrier of F2() & F3(x) in { F3(z) where z is Element of F1() : P1[z] } ) by A5; hence y in F4() .: { F3(x) where x is Element of F1() : P1[x] } by A1, A4, FUNCT_1:def_6; ::_thesis: verum end; Lm1: for S being non empty RelStr for D being non empty Subset of S holds D = { i where i is Element of S : i in D } proof let S be non empty RelStr ; ::_thesis: for D being non empty Subset of S holds D = { i where i is Element of S : i in D } let D be non empty Subset of S; ::_thesis: D = { i where i is Element of S : i in D } thus D c= { i where i is Element of S : i in D } :: according to XBOOLE_0:def_10 ::_thesis: { i where i is Element of S : i in D } c= D proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in { i where i is Element of S : i in D } ) assume a in D ; ::_thesis: a in { i where i is Element of S : i in D } hence a in { i where i is Element of S : i in D } ; ::_thesis: verum end; thus { i where i is Element of S : i in D } c= D ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { i where i is Element of S : i in D } or a in D ) assume a in { i where i is Element of S : i in D } ; ::_thesis: a in D then ex j being Element of S st ( j = a & j in D ) ; hence a in D ; ::_thesis: verum end; end; theorem Th29: :: WAYBEL24:29 for S, T being complete Scott TopLattice for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T proof let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T let F be non empty Subset of (ContMaps (S,T)); ::_thesis: "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3; then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13; then reconsider F9 = F as Subset of (T |^ the carrier of S) by XBOOLE_1:1; reconsider sF = sup F9 as Function of S,T by Th6; now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_ sF_._x_<=_sF_._y let x, y be Element of S; ::_thesis: ( x <= y implies sF . x <= sF . y ) set G1 = { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ; assume A1: x <= y ; ::_thesis: sF . x <= sF . y A2: { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } is_<=_than sF . y proof let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } or a <= sF . y ) assume a in { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ; ::_thesis: a <= sF . y then consider f9 being Element of (T |^ the carrier of S) such that A3: a = f9 . x and A4: f9 in F9 ; reconsider f1 = f9 as continuous Function of S,T by A4, Th21; reconsider f1 = f1 as monotone Function of S,T ; f9 <= sup F9 by A4, YELLOW_2:22; then f1 <= sF by WAYBEL10:11; then A5: f1 . y <= sF . y by YELLOW_2:9; f1 . x <= f1 . y by A1, WAYBEL_1:def_2; hence a <= sF . y by A3, A5, YELLOW_0:def_2; ::_thesis: verum end; sF . x = "\/" ( { (f . x) where f is Element of (T |^ the carrier of S) : f in F9 } ,T) by Th25; hence sF . x <= sF . y by A2, YELLOW_0:32; ::_thesis: verum end; hence "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T by WAYBEL_1:def_2; ::_thesis: verum end; theorem Th30: :: WAYBEL24:30 for S, T being complete Scott TopLattice for F being non empty Subset of (ContMaps (S,T)) for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) proof let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty directed Subset of S holds "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) let D be non empty directed Subset of S; ::_thesis: "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) reconsider sF = "\/" (F,(T |^ the carrier of S)) as Function of S,T by Th19; set F9 = F; set L = "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T); set P = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T); set L1 = { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ; set P1 = { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } ; reconsider L = "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T), P = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) as Element of T ; defpred S1[ set ] means \$1 in F; deffunc H1( Element of S) -> Element of S = \$1; defpred S2[ set ] means \$1 in D; deffunc H2( Element of (T |^ the carrier of S)) -> Element of the carrier of T = "\/" ( { (\$1 . i4) where i4 is Element of S : i4 in D } ,T); deffunc H3( Element of (T |^ the carrier of S)) -> set = \$1 . (sup D); A1: P = sup (sF .: D) by Th28; { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } is_<=_than P proof let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } or b <= P ) assume b in { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ; ::_thesis: b <= P then consider g9 being Element of (T |^ the carrier of S) such that A2: b = "\/" ( { (g9 . i) where i is Element of S : i in D } ,T) and A3: g9 in F ; reconsider g1 = g9 as continuous Function of S,T by A3, Th21; g9 <= "\/" (F,(T |^ the carrier of S)) by A3, YELLOW_2:22; then A4: g1 <= sF by WAYBEL10:11; A5: g1 .: D is_<=_than sup (sF .: D) proof let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in g1 .: D or a <= sup (sF .: D) ) assume a in g1 .: D ; ::_thesis: a <= sup (sF .: D) then consider x being set such that A6: x in dom g1 and A7: x in D and A8: a = g1 . x by FUNCT_1:def_6; reconsider x9 = x as Element of S by A6; x in the carrier of S by A6; then x9 in dom sF by FUNCT_2:def_1; then sF . x9 in sF .: D by A7, FUNCT_1:def_6; then A9: sF . x9 <= sup (sF .: D) by YELLOW_2:22; g1 . x9 <= sF . x9 by A4, YELLOW_2:9; hence a <= sup (sF .: D) by A8, A9, YELLOW_0:def_2; ::_thesis: verum end; the carrier of S c= dom g1 by FUNCT_2:def_1; then A10: the carrier of S c= dom g9 ; g9 .: { H1(i2) where i2 is Element of S : S2[i2] } = { (g9 . H1(i)) where i is Element of S : S2[i] } from WAYBEL24:sch_5(A10); then b = "\/" ((g9 .: D),T) by A2, Lm1; hence b <= P by A1, A5, YELLOW_0:32; ::_thesis: verum end; then A11: L <= P by YELLOW_0:32; A12: for g8 being Element of (T |^ the carrier of S) st S1[g8] holds H2(g8) = H3(g8) proof let g1 be Element of (T |^ the carrier of S); ::_thesis: ( S1[g1] implies H2(g1) = H3(g1) ) assume g1 in F ; ::_thesis: H2(g1) = H3(g1) then reconsider g9 = g1 as continuous Function of S,T by Th21; A13: ( g9 preserves_sup_of D & ex_sup_of D,S ) by WAYBEL_0:def_37, YELLOW_0:17; the carrier of S c= dom g9 by FUNCT_2:def_1; then A14: the carrier of S c= dom g1 ; g1 .: { H1(i2) where i2 is Element of S : S2[i2] } = { (g1 . H1(i)) where i is Element of S : S2[i] } from WAYBEL24:sch_5(A14); then "\/" ( { (g1 . i) where i is Element of S : i in D } ,T) = sup (g9 .: D) by Lm1 .= g1 . (sup D) by A13, WAYBEL_0:def_31 ; hence H2(g1) = H3(g1) ; ::_thesis: verum end; { H2(g3) where g3 is Element of (T |^ the carrier of S) : S1[g3] } = { H3(g4) where g4 is Element of (T |^ the carrier of S) : S1[g4] } from WAYBEL24:sch_4(A12); then A15: L = sF . (sup D) by Th26; { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } is_<=_than L proof let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } or b <= L ) assume b in { ("\/" ( { (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F } ,T)) where i3 is Element of S : i3 in D } ; ::_thesis: b <= L then consider i9 being Element of S such that A16: b = "\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T) and A17: i9 in D ; i9 in the carrier of S ; then A18: i9 in dom sF by FUNCT_2:def_1; b = sF . i9 by A16, Th26; then b in sF .: D by A17, A18, FUNCT_1:def_6; then A19: b <= sup (sF .: D) by YELLOW_2:22; sF is monotone by Th29; then sup (sF .: D) <= L by A15, WAYBEL17:15; hence b <= L by A19, YELLOW_0:def_2; ::_thesis: verum end; then P <= L by YELLOW_0:32; hence "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) by A11, YELLOW_0:def_3; ::_thesis: verum end; theorem Th31: :: WAYBEL24:31 for S, T being complete Scott TopLattice for F being non empty Subset of (ContMaps (S,T)) for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) proof let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) let D be non empty directed Subset of S; ::_thesis: "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3; then the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13; then reconsider F9 = F as non empty Subset of (T |^ the carrier of S) by XBOOLE_1:1; reconsider sF = sup F9 as Function of S,T by Th19; set L = "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T); set P = "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T); deffunc H1( Element of (T |^ the carrier of S)) -> Element of the carrier of T = "\/" ( { (\$1 . i4) where i4 is Element of S : i4 in D } ,T); deffunc H2( Element of (T |^ the carrier of S)) -> set = \$1 . (sup D); defpred S1[ set ] means \$1 in F9; A1: for g8 being Element of (T |^ the carrier of S) st S1[g8] holds H1(g8) = H2(g8) proof deffunc H3( Element of S) -> Element of S = \$1; let g1 be Element of (T |^ the carrier of S); ::_thesis: ( S1[g1] implies H1(g1) = H2(g1) ) assume g1 in F9 ; ::_thesis: H1(g1) = H2(g1) then reconsider g9 = g1 as continuous Function of S,T by Th21; defpred S2[ set ] means \$1 in D; A2: ( g9 preserves_sup_of D & ex_sup_of D,S ) by WAYBEL_0:def_37, YELLOW_0:17; the carrier of S c= dom g9 by FUNCT_2:def_1; then A3: the carrier of S c= dom g1 ; g1 .: { H3(i2) where i2 is Element of S : S2[i2] } = { (g1 . H3(i)) where i is Element of S : S2[i] } from WAYBEL24:sch_5(A3); then "\/" ( { (g1 . i) where i is Element of S : i in D } ,T) = sup (g9 .: D) by Lm1 .= g1 . (sup D) by A2, WAYBEL_0:def_31 ; hence H1(g1) = H2(g1) ; ::_thesis: verum end; { H1(g3) where g3 is Element of (T |^ the carrier of S) : S1[g3] } = { H2(g4) where g4 is Element of (T |^ the carrier of S) : S1[g4] } from WAYBEL24:sch_4(A1); then A4: "\/" ( { ("\/" ( { (g . i) where i is Element of S : i in D } ,T)) where g is Element of (T |^ the carrier of S) : g in F } ,T) = sF . (sup D) by Th25; "\/" ( { ("\/" ( { (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F } ,T)) where i9 is Element of S : i9 in D } ,T) = sup (sF .: D) by Th27; hence "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) by A4, Th30; ::_thesis: verum end; theorem Th32: :: WAYBEL24:32 for S, T being complete Scott TopLattice for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) proof let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) let F be non empty Subset of (ContMaps (S,T)); ::_thesis: "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) reconsider Ex = "\/" (F,(T |^ the carrier of S)) as Function of S,T by Th19; for X being Subset of S st not X is empty & X is directed holds Ex preserves_sup_of X proof let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies Ex preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: Ex preserves_sup_of X then reconsider X9 = X as non empty directed Subset of S ; Ex preserves_sup_of X9 proof assume ex_sup_of X9,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of Ex .: X9,T & "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) ) thus ex_sup_of Ex .: X9,T by YELLOW_0:17; ::_thesis: "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) thus "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) by Th31; ::_thesis: verum end; hence Ex preserves_sup_of X ; ::_thesis: verum end; then Ex is directed-sups-preserving by WAYBEL_0:def_37; hence "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) by Def3; ::_thesis: verum end; theorem Th33: :: WAYBEL24:33 for S being non empty RelStr for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T) proof let S be non empty RelStr ; ::_thesis: for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T) let T be non empty antisymmetric lower-bounded RelStr ; ::_thesis: Bottom (T |^ the carrier of S) = S --> (Bottom T) set L = T |^ the carrier of S; reconsider f = S --> (Bottom T) as Element of (T |^ the carrier of S) by Th19; reconsider f9 = f as Function of S,T ; A1: for b being Element of (T |^ the carrier of S) st b is_>=_than {} holds f <= b proof let b be Element of (T |^ the carrier of S); ::_thesis: ( b is_>=_than {} implies f <= b ) reconsider b9 = b as Function of S,T by Th19; assume b is_>=_than {} ; ::_thesis: f <= b for x being Element of S holds f9 . x <= b9 . x proof let x be Element of S; ::_thesis: f9 . x <= b9 . x f9 . x = ( the carrier of S --> (Bottom T)) . x .= Bottom T by FUNCOP_1:7 ; hence f9 . x <= b9 . x by YELLOW_0:44; ::_thesis: verum end; then f9 <= b9 by YELLOW_2:9; hence f <= b by WAYBEL10:11; ::_thesis: verum end; f is_>=_than {} by YELLOW_0:6; then f = "\/" ({},(T |^ the carrier of S)) by A1, YELLOW_0:30; hence Bottom (T |^ the carrier of S) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum end; theorem :: WAYBEL24:34 for S being non empty RelStr for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T) proof let S be non empty RelStr ; ::_thesis: for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T) let T be non empty antisymmetric upper-bounded RelStr ; ::_thesis: Top (T |^ the carrier of S) = S --> (Top T) set L = T |^ the carrier of S; reconsider f = S --> (Top T) as Element of (T |^ the carrier of S) by Th19; reconsider f9 = f as Function of S,T ; A1: for b being Element of (T |^ the carrier of S) st b is_<=_than {} holds f >= b proof let b be Element of (T |^ the carrier of S); ::_thesis: ( b is_<=_than {} implies f >= b ) reconsider b9 = b as Function of S,T by Th19; assume b is_<=_than {} ; ::_thesis: f >= b for x being Element of S holds f9 . x >= b9 . x proof let x be Element of S; ::_thesis: f9 . x >= b9 . x f9 . x = ( the carrier of S --> (Top T)) . x .= Top T by FUNCOP_1:7 ; hence f9 . x >= b9 . x by YELLOW_0:45; ::_thesis: verum end; then f9 >= b9 by YELLOW_2:9; hence f >= b by WAYBEL10:11; ::_thesis: verum end; f is_<=_than {} by YELLOW_0:6; then f = "/\" ({},(T |^ the carrier of S)) by A1, YELLOW_0:31; hence Top (T |^ the carrier of S) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum end; registration let S be non empty reflexive RelStr ; let T be complete LATTICE; let a be Element of T; clusterS --> a -> directed-sups-preserving ; coherence S --> a is directed-sups-preserving proof set f = S --> a; for X being Subset of S st not X is empty & X is directed holds S --> a preserves_sup_of X proof let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies S --> a preserves_sup_of X ) assume ( not X is empty & X is directed ) ; ::_thesis: S --> a preserves_sup_of X then reconsider X9 = X as non empty directed Subset of S ; S --> a preserves_sup_of X proof assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (S --> a) .: X,T & "\/" (((S --> a) .: X),T) = (S --> a) . ("\/" (X,S)) ) thus ex_sup_of (S --> a) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((S --> a) .: X),T) = (S --> a) . ("\/" (X,S)) A1: {a} c= (S --> a) .: X proof set n = the Element of X9; let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in {a} or b in (S --> a) .: X ) A2: a = ( the carrier of S --> a) . the Element of X9 by FUNCOP_1:7 .= (S --> a) . the Element of X9 ; assume b in {a} ; ::_thesis: b in (S --> a) .: X then A3: b = a by TARSKI:def_1; dom (S --> a) = the carrier of S by FUNCOP_1:13; hence b in (S --> a) .: X by A3, A2, FUNCT_1:def_6; ::_thesis: verum end; (S --> a) .: X c= rng (S --> a) by RELAT_1:111; then (S --> a) .: X c= {a} by FUNCOP_1:8; hence sup ((S --> a) .: X) = sup {a} by A1, XBOOLE_0:def_10 .= a by YELLOW_0:39 .= ( the carrier of S --> a) . (sup X) by FUNCOP_1:7 .= (S --> a) . (sup X) ; ::_thesis: verum end; hence S --> a preserves_sup_of X ; ::_thesis: verum end; hence S --> a is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum end; end; theorem Th35: :: WAYBEL24:35 for S, T being complete Scott TopLattice holds ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S proof let S, T be complete Scott TopLattice; ::_thesis: ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S set L = T |^ the carrier of S; reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3; now__::_thesis:_for_X_being_Subset_of_CS_st_ex_sup_of_X,T_|^_the_carrier_of_S_holds_ "\/"_(X,(T_|^_the_carrier_of_S))_in_the_carrier_of_CS let X be Subset of CS; ::_thesis: ( ex_sup_of X,T |^ the carrier of S implies "\/" (b1,(T |^ the carrier of S)) in the carrier of CS ) assume ex_sup_of X,T |^ the carrier of S ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS percases ( not X is empty or X is empty ) ; suppose not X is empty ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS hence "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Th32; ::_thesis: verum end; suppose X is empty ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS then "\/" (X,(T |^ the carrier of S)) = Bottom (T |^ the carrier of S) by YELLOW_0:def_11; then "\/" (X,(T |^ the carrier of S)) = S --> (Bottom T) by Th33; hence "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Def3; ::_thesis: verum end; end; end; hence ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S by YELLOW_0:def_19; ::_thesis: verum end; registration let S, T be complete Scott TopLattice; cluster ContMaps (S,T) -> strict complete ; coherence ContMaps (S,T) is complete proof ContMaps (S,T) is non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def3, Th35; hence ContMaps (S,T) is complete by YELLOW_2:31; ::_thesis: verum end; end; theorem :: WAYBEL24:36 for S, T being non empty complete Scott TopLattice holds Bottom (ContMaps (S,T)) = S --> (Bottom T) proof let S, T be non empty complete Scott TopLattice; ::_thesis: Bottom (ContMaps (S,T)) = S --> (Bottom T) set L = ContMaps (S,T); reconsider f = S --> (Bottom T) as Element of (ContMaps (S,T)) by Th21; reconsider f9 = f as Function of S,T ; A1: for b being Element of (ContMaps (S,T)) st b is_>=_than {} holds f <= b proof let b be Element of (ContMaps (S,T)); ::_thesis: ( b is_>=_than {} implies f <= b ) reconsider b9 = b as Function of S,T by Th21; assume b is_>=_than {} ; ::_thesis: f <= b for i being Element of S holds [(f . i),(b . i)] in the InternalRel of T proof let i be Element of S; ::_thesis: [(f . i),(b . i)] in the InternalRel of T f . i = ( the carrier of S --> (Bottom T)) . i .= Bottom T by FUNCOP_1:7 ; then f9 . i <= b9 . i by YELLOW_0:44; hence [(f . i),(b . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum end; hence f <= b by Th20; ::_thesis: verum end; f is_>=_than {} by YELLOW_0:6; then f = "\/" ({},(ContMaps (S,T))) by A1, YELLOW_0:30; hence Bottom (ContMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum end; theorem :: WAYBEL24:37 for S, T being non empty complete Scott TopLattice holds Top (ContMaps (S,T)) = S --> (Top T) proof let S, T be non empty complete Scott TopLattice; ::_thesis: Top (ContMaps (S,T)) = S --> (Top T) set L = ContMaps (S,T); reconsider f = S --> (Top T) as Element of (ContMaps (S,T)) by Th21; reconsider f9 = f as Function of S,T ; A1: for b being Element of (ContMaps (S,T)) st b is_<=_than {} holds f >= b proof let b be Element of (ContMaps (S,T)); ::_thesis: ( b is_<=_than {} implies f >= b ) reconsider b9 = b as Function of S,T by Th21; assume b is_<=_than {} ; ::_thesis: f >= b for i being Element of S holds [(b . i),(f . i)] in the InternalRel of T proof let i be Element of S; ::_thesis: [(b . i),(f . i)] in the InternalRel of T f . i = ( the carrier of S --> (Top T)) . i .= Top T by FUNCOP_1:7 ; then f9 . i >= b9 . i by YELLOW_0:45; hence [(b . i),(f . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum end; hence f >= b by Th20; ::_thesis: verum end; f is_<=_than {} by YELLOW_0:6; then f = "/\" ({},(ContMaps (S,T))) by A1, YELLOW_0:31; hence Top (ContMaps (S,T)) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum end; theorem :: WAYBEL24:38 for S, T being complete Scott TopLattice holds SCMaps (S,T) = ContMaps (S,T) proof let S, T be complete Scott TopLattice; ::_thesis: SCMaps (S,T) = ContMaps (S,T) reconsider Sm = ContMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by Def3; reconsider SC = SCMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by WAYBEL15:1; A1: the carrier of SC c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13; A2: the carrier of SC c= the carrier of Sm proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of SC or a in the carrier of Sm ) assume A3: a in the carrier of SC ; ::_thesis: a in the carrier of Sm then reconsider f = a as Function of S,T by A1, WAYBEL10:9; f is continuous Function of S,T by A3, WAYBEL17:def_2; then a is Element of Sm by Th21; hence a in the carrier of Sm ; ::_thesis: verum end; the carrier of Sm c= the carrier of SC proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of Sm or a in the carrier of SC ) assume a in the carrier of Sm ; ::_thesis: a in the carrier of SC then a is continuous Function of S,T by Th21; hence a in the carrier of SC by WAYBEL17:def_2; ::_thesis: verum end; then the carrier of SC = the carrier of Sm by A2, XBOOLE_0:def_10; hence SCMaps (S,T) = ContMaps (S,T) by YELLOW_0:57; ::_thesis: verum end;