:: WAYBEL27 semantic presentation begin definition let F be Function; attrF is uncurrying means :Def1: :: WAYBEL27:def 1 ( ( for x being set st x in dom F holds x is Function-yielding Function ) & ( for f being Function st f in dom F holds F . f = uncurry f ) ); attrF is currying means :Def2: :: WAYBEL27:def 2 ( ( for x being set st x in dom F holds ( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds F . f = curry f ) ); attrF is commuting means :Def3: :: WAYBEL27:def 3 ( ( for x being set st x in dom F holds x is Function-yielding Function ) & ( for f being Function st f in dom F holds F . f = commute f ) ); end; :: deftheorem Def1 defines uncurrying WAYBEL27:def_1_:_ for F being Function holds ( F is uncurrying iff ( ( for x being set st x in dom F holds x is Function-yielding Function ) & ( for f being Function st f in dom F holds F . f = uncurry f ) ) ); :: deftheorem Def2 defines currying WAYBEL27:def_2_:_ for F being Function holds ( F is currying iff ( ( for x being set st x in dom F holds ( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds F . f = curry f ) ) ); :: deftheorem Def3 defines commuting WAYBEL27:def_3_:_ for F being Function holds ( F is commuting iff ( ( for x being set st x in dom F holds x is Function-yielding Function ) & ( for f being Function st f in dom F holds F . f = commute f ) ) ); registration cluster empty Relation-like Function-like -> uncurrying currying commuting for set ; coherence for b1 being Function st b1 is empty holds ( b1 is uncurrying & b1 is currying & b1 is commuting ) proof let F be Function; ::_thesis: ( F is empty implies ( F is uncurrying & F is currying & F is commuting ) ) assume A1: F is empty ; ::_thesis: ( F is uncurrying & F is currying & F is commuting ) hence for x being set st x in dom F holds x is Function-yielding Function ; :: according to WAYBEL27:def_1 ::_thesis: ( ( for f being Function st f in dom F holds F . f = uncurry f ) & F is currying & F is commuting ) thus for f being Function st f in dom F holds F . f = uncurry f by A1; ::_thesis: ( F is currying & F is commuting ) thus for x being set st x in dom F holds ( x is Function & proj1 x is Relation ) by A1; :: according to WAYBEL27:def_2 ::_thesis: ( ( for f being Function st f in dom F holds F . f = curry f ) & F is commuting ) thus for f being Function st f in dom F holds F . f = curry f by A1; ::_thesis: F is commuting thus for x being set st x in dom F holds x is Function-yielding Function by A1; :: according to WAYBEL27:def_3 ::_thesis: for f being Function st f in dom F holds F . f = commute f thus for f being Function st f in dom F holds F . f = commute f by A1; ::_thesis: verum end; end; registration cluster Relation-like Function-like uncurrying currying commuting for set ; existence ex b1 being Function st ( b1 is uncurrying & b1 is currying & b1 is commuting ) proof reconsider F = {} as Function ; take F ; ::_thesis: ( F is uncurrying & F is currying & F is commuting ) thus ( F is uncurrying & F is currying & F is commuting ) ; ::_thesis: verum end; end; registration let F be uncurrying Function; let X be set ; clusterF | X -> uncurrying ; coherence F | X is uncurrying proof A1: for f being Function st f in dom (F | X) holds (F | X) . f = uncurry f proof let f be Function; ::_thesis: ( f in dom (F | X) implies (F | X) . f = uncurry f ) assume A2: f in dom (F | X) ; ::_thesis: (F | X) . f = uncurry f then A3: f in dom F by RELAT_1:57; thus (F | X) . f = F . f by A2, FUNCT_1:47 .= uncurry f by A3, Def1 ; ::_thesis: verum end; for x being set st x in dom (F | X) holds x is Function-yielding Function proof let x be set ; ::_thesis: ( x in dom (F | X) implies x is Function-yielding Function ) assume x in dom (F | X) ; ::_thesis: x is Function-yielding Function then x in dom F by RELAT_1:57; hence x is Function-yielding Function by Def1; ::_thesis: verum end; hence F | X is uncurrying by A1, Def1; ::_thesis: verum end; end; registration let F be currying Function; let X be set ; clusterF | X -> currying ; coherence F | X is currying proof A1: for f being Function st f in dom (F | X) holds (F | X) . f = curry f proof let f be Function; ::_thesis: ( f in dom (F | X) implies (F | X) . f = curry f ) assume A2: f in dom (F | X) ; ::_thesis: (F | X) . f = curry f then A3: f in dom F by RELAT_1:57; thus (F | X) . f = F . f by A2, FUNCT_1:47 .= curry f by A3, Def2 ; ::_thesis: verum end; for x being set st x in dom (F | X) holds ( x is Function & proj1 x is Relation ) proof let x be set ; ::_thesis: ( x in dom (F | X) implies ( x is Function & proj1 x is Relation ) ) assume x in dom (F | X) ; ::_thesis: ( x is Function & proj1 x is Relation ) then x in dom F by RELAT_1:57; hence ( x is Function & proj1 x is Relation ) by Def2; ::_thesis: verum end; hence F | X is currying by A1, Def2; ::_thesis: verum end; end; theorem Th1: :: WAYBEL27:1 for X, Y, Z, D being set st D c= Funcs (X,(Funcs (Y,Z))) holds ex F being ManySortedSet of D st ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) proof let X, Y, Z, D be set ; ::_thesis: ( D c= Funcs (X,(Funcs (Y,Z))) implies ex F being ManySortedSet of D st ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) ) assume A1: D c= Funcs (X,(Funcs (Y,Z))) ; ::_thesis: ex F being ManySortedSet of D st ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) percases ( D is empty or not D is empty ) ; suppose D is empty ; ::_thesis: ex F being ManySortedSet of D st ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) then reconsider F = {} as ManySortedSet of D by PARTFUN1:def_2, RELAT_1:38, RELAT_1:def_18; take F ; ::_thesis: ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) thus F is uncurrying ; ::_thesis: rng F c= Funcs ([:X,Y:],Z) thus rng F c= Funcs ([:X,Y:],Z) by RELAT_1:38, XBOOLE_1:2; ::_thesis: verum end; suppose not D is empty ; ::_thesis: ex F being ManySortedSet of D st ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) then reconsider E = D as non empty functional set by A1; deffunc H1( Function) -> set = uncurry \$1; consider F being ManySortedSet of E such that A2: for d being Element of E holds F . d = H1(d) from PBOOLE:sch_5(); reconsider F1 = F as ManySortedSet of D ; take F1 ; ::_thesis: ( F1 is uncurrying & rng F1 c= Funcs ([:X,Y:],Z) ) thus F1 is uncurrying ::_thesis: rng F1 c= Funcs ([:X,Y:],Z) proof hereby :: according to WAYBEL27:def_1 ::_thesis: for f being Function st f in dom F1 holds F1 . f = uncurry f let x be set ; ::_thesis: ( x in dom F1 implies x is Function-yielding Function ) assume x in dom F1 ; ::_thesis: x is Function-yielding Function then x in D ; then consider x1 being Function such that A3: x1 = x and dom x1 = X and A4: rng x1 c= Funcs (Y,Z) by A1, FUNCT_2:def_2; x1 is Function-yielding proof let a be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not a in proj1 x1 or x1 . a is set ) assume a in dom x1 ; ::_thesis: x1 . a is set then x1 . a in rng x1 by FUNCT_1:def_3; hence x1 . a is set by A4; ::_thesis: verum end; hence x is Function-yielding Function by A3; ::_thesis: verum end; let f be Function; ::_thesis: ( f in dom F1 implies F1 . f = uncurry f ) assume f in dom F1 ; ::_thesis: F1 . f = uncurry f then reconsider d = f as Element of E ; thus F1 . f = F . d .= uncurry f by A2 ; ::_thesis: verum end; thus rng F1 c= Funcs ([:X,Y:],Z) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F1 or y in Funcs ([:X,Y:],Z) ) assume y in rng F1 ; ::_thesis: y in Funcs ([:X,Y:],Z) then consider x being set such that A5: x in dom F1 and A6: y = F1 . x by FUNCT_1:def_3; reconsider d = x as Element of E by A5; A7: d in Funcs (X,(Funcs (Y,Z))) by A1, TARSKI:def_3; y = uncurry d by A2, A6; hence y in Funcs ([:X,Y:],Z) by A7, FUNCT_6:11; ::_thesis: verum end; end; end; end; theorem Th2: :: WAYBEL27:2 for X, Y, Z, D being set st D c= Funcs ([:X,Y:],Z) holds ex F being ManySortedSet of D st ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) proof let X, Y, Z, D be set ; ::_thesis: ( D c= Funcs ([:X,Y:],Z) implies ex F being ManySortedSet of D st ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) ) assume A1: D c= Funcs ([:X,Y:],Z) ; ::_thesis: ex F being ManySortedSet of D st ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) percases ( D is empty or not D is empty ) ; suppose D is empty ; ::_thesis: ex F being ManySortedSet of D st ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) then reconsider F = {} as ManySortedSet of D by PARTFUN1:def_2, RELAT_1:38, RELAT_1:def_18; take F ; ::_thesis: ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) thus F is currying ; ::_thesis: ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) assume ( Y = {} implies X = {} ) ; ::_thesis: rng F c= Funcs (X,(Funcs (Y,Z))) thus rng F c= Funcs (X,(Funcs (Y,Z))) by RELAT_1:38, XBOOLE_1:2; ::_thesis: verum end; suppose not D is empty ; ::_thesis: ex F being ManySortedSet of D st ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) then reconsider E = D as non empty functional set by A1; deffunc H1( Function) -> set = curry \$1; consider F being ManySortedSet of E such that A2: for d being Element of E holds F . d = H1(d) from PBOOLE:sch_5(); reconsider F1 = F as ManySortedSet of D ; take F1 ; ::_thesis: ( F1 is currying & ( ( Y = {} implies X = {} ) implies rng F1 c= Funcs (X,(Funcs (Y,Z))) ) ) thus F1 is currying ::_thesis: ( ( Y = {} implies X = {} ) implies rng F1 c= Funcs (X,(Funcs (Y,Z))) ) proof hereby :: according to WAYBEL27:def_2 ::_thesis: for f being Function st f in dom F1 holds F1 . f = curry f let x be set ; ::_thesis: ( x in dom F1 implies ( x is Function & proj1 x is Relation ) ) assume x in dom F1 ; ::_thesis: ( x is Function & proj1 x is Relation ) then A3: x in D ; hence x is Function by A1; ::_thesis: proj1 x is Relation ex x1 being Function st ( x1 = x & dom x1 = [:X,Y:] & rng x1 c= Z ) by A3, A1, FUNCT_2:def_2; hence proj1 x is Relation ; ::_thesis: verum end; let f be Function; ::_thesis: ( f in dom F1 implies F1 . f = curry f ) assume f in dom F1 ; ::_thesis: F1 . f = curry f then reconsider d = f as Element of E ; thus F1 . f = F . d .= curry f by A2 ; ::_thesis: verum end; assume A4: ( Y = {} implies X = {} ) ; ::_thesis: rng F1 c= Funcs (X,(Funcs (Y,Z))) thus rng F1 c= Funcs (X,(Funcs (Y,Z))) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F1 or y in Funcs (X,(Funcs (Y,Z))) ) assume y in rng F1 ; ::_thesis: y in Funcs (X,(Funcs (Y,Z))) then consider x being set such that A5: x in dom F1 and A6: y = F1 . x by FUNCT_1:def_3; reconsider d = x as Element of E by A5; A7: y = curry d by A2, A6; A8: d in Funcs ([:X,Y:],Z) by A1, TARSKI:def_3; percases ( [:X,Y:] = {} or [:X,Y:] <> {} ) ; supposeA9: [:X,Y:] = {} ; ::_thesis: y in Funcs (X,(Funcs (Y,Z))) then A10: d is Function of {},Z by A8, FUNCT_2:66; now__::_thesis:_(_X_=_{}_implies_y_in_Funcs_(X,(Funcs_(Y,Z)))_) assume A11: X = {} ; ::_thesis: y in Funcs (X,(Funcs (Y,Z))) then y is Function of X,(Funcs (Y,Z)) by A7, A10, FUNCT_5:42, RELSET_1:12; hence y in Funcs (X,(Funcs (Y,Z))) by A11, FUNCT_2:8; ::_thesis: verum end; hence y in Funcs (X,(Funcs (Y,Z))) by A4, A9; ::_thesis: verum end; suppose [:X,Y:] <> {} ; ::_thesis: y in Funcs (X,(Funcs (Y,Z))) hence y in Funcs (X,(Funcs (Y,Z))) by A7, A8, FUNCT_6:10; ::_thesis: verum end; end; end; end; end; end; registration let X, Y, Z be set ; cluster Relation-like Funcs (X,(Funcs (Y,Z))) -defined Function-like V27( Funcs (X,(Funcs (Y,Z)))) uncurrying for set ; existence ex b1 being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st b1 is uncurrying proof ex F being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st ( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) ) by Th1; hence ex b1 being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st b1 is uncurrying ; ::_thesis: verum end; cluster Relation-like Funcs ([:X,Y:],Z) -defined Function-like V27( Funcs ([:X,Y:],Z)) currying for set ; existence ex b1 being ManySortedSet of Funcs ([:X,Y:],Z) st b1 is currying proof ex F being ManySortedSet of Funcs ([:X,Y:],Z) st ( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) ) by Th2; hence ex b1 being ManySortedSet of Funcs ([:X,Y:],Z) st b1 is currying ; ::_thesis: verum end; end; theorem Th3: :: WAYBEL27:3 for A, B being non empty set for C being set for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) proof let A, B be non empty set ; ::_thesis: for C being set for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) let C be set ; ::_thesis: for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) let f, g be commuting Function; ::_thesis: ( dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g implies g * f = id (dom f) ) assume that A1: dom f c= Funcs (A,(Funcs (B,C))) and A2: rng f c= dom g ; ::_thesis: g * f = id (dom f) A3: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (g_*_f)_._x_=_x let x be set ; ::_thesis: ( x in dom f implies (g * f) . x = x ) assume A4: x in dom f ; ::_thesis: (g * f) . x = x then reconsider X = x as Function by Def3; A5: f . x in rng f by A4, FUNCT_1:def_3; then reconsider Y = f . x as Function by A2, Def3; thus (g * f) . x = g . (f . x) by A4, FUNCT_1:13 .= commute Y by A2, A5, Def3 .= commute (commute X) by A4, Def3 .= x by A1, A4, FUNCT_6:57 ; ::_thesis: verum end; dom (g * f) = dom f by A2, RELAT_1:27; hence g * f = id (dom f) by A3, FUNCT_1:17; ::_thesis: verum end; theorem Th4: :: WAYBEL27:4 for B being non empty set for A, C being set for f being uncurrying Function for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) proof let B be non empty set ; ::_thesis: for A, C being set for f being uncurrying Function for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) let A, C be set ; ::_thesis: for f being uncurrying Function for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) let f be uncurrying Function; ::_thesis: for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds g * f = id (dom f) let g be currying Function; ::_thesis: ( dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g implies g * f = id (dom f) ) assume that A1: dom f c= Funcs (A,(Funcs (B,C))) and A2: rng f c= dom g ; ::_thesis: g * f = id (dom f) A3: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (g_*_f)_._x_=_x let x be set ; ::_thesis: ( x in dom f implies (g * f) . x = x ) assume A4: x in dom f ; ::_thesis: (g * f) . x = x then reconsider X = x as Function by Def1; A5: ex F being Function st ( X = F & dom F = A & rng F c= Funcs (B,C) ) by A1, A4, FUNCT_2:def_2; A6: f . x in rng f by A4, FUNCT_1:def_3; then reconsider Y = f . x as Function by A2, Def2; thus (g * f) . x = g . (f . x) by A4, FUNCT_1:13 .= curry Y by A2, A6, Def2 .= curry (uncurry X) by A4, Def1 .= x by A5, FUNCT_5:48 ; ::_thesis: verum end; dom (g * f) = dom f by A2, RELAT_1:27; hence g * f = id (dom f) by A3, FUNCT_1:17; ::_thesis: verum end; theorem Th5: :: WAYBEL27:5 for A, B, C being set for f being currying Function for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds g * f = id (dom f) proof let A, B, C be set ; ::_thesis: for f being currying Function for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds g * f = id (dom f) let f be currying Function; ::_thesis: for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds g * f = id (dom f) let g be uncurrying Function; ::_thesis: ( dom f c= Funcs ([:A,B:],C) & rng f c= dom g implies g * f = id (dom f) ) assume that A1: dom f c= Funcs ([:A,B:],C) and A2: rng f c= dom g ; ::_thesis: g * f = id (dom f) A3: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ (g_*_f)_._x_=_x let x be set ; ::_thesis: ( x in dom f implies (g * f) . x = x ) assume A4: x in dom f ; ::_thesis: (g * f) . x = x then reconsider X = x as Function by Def2; A5: ex F being Function st ( X = F & dom F = [:A,B:] & rng F c= C ) by A1, A4, FUNCT_2:def_2; A6: f . x in rng f by A4, FUNCT_1:def_3; then reconsider Y = f . x as Function by A2, Def1; thus (g * f) . x = g . (f . x) by A4, FUNCT_1:13 .= uncurry Y by A2, A6, Def1 .= uncurry (curry X) by A4, Def2 .= x by A5, FUNCT_5:49 ; ::_thesis: verum end; dom (g * f) = dom f by A2, RELAT_1:27; hence g * f = id (dom f) by A3, FUNCT_1:17; ::_thesis: verum end; theorem Th6: :: WAYBEL27:6 for f being Function-yielding Function for i, A being set st i in dom (commute f) holds ((commute f) . i) .: A c= pi ((f .: A),i) proof let f be Function-yielding Function; ::_thesis: for i, A being set st i in dom (commute f) holds ((commute f) . i) .: A c= pi ((f .: A),i) let i, A be set ; ::_thesis: ( i in dom (commute f) implies ((commute f) . i) .: A c= pi ((f .: A),i) ) A1: commute f = curry' (uncurry f) by FUNCT_6:def_10 .= curry (~ (uncurry f)) by FUNCT_5:def_3 ; assume A2: i in dom (commute f) ; ::_thesis: ((commute f) . i) .: A c= pi ((f .: A),i) thus ((commute f) . i) .: A c= pi ((f .: A),i) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((commute f) . i) .: A or x in pi ((f .: A),i) ) assume x in ((commute f) . i) .: A ; ::_thesis: x in pi ((f .: A),i) then consider y being set such that A3: y in dom ((commute f) . i) and A4: y in A and A5: x = ((commute f) . i) . y by FUNCT_1:def_6; A6: [i,y] in dom (~ (uncurry f)) by A2, A1, A3, FUNCT_5:31; then A7: [y,i] in dom (uncurry f) by FUNCT_4:42; then ex a being set ex g being Function ex b being set st ( [y,i] = [a,b] & a in dom f & g = f . a & b in dom g ) by FUNCT_5:def_2; then y in dom f by XTUPLE_0:1; then A8: f . y in f .: A by A4, FUNCT_1:def_6; A9: [y,i] `2 = i ; A10: [y,i] `1 = y ; x = (~ (uncurry f)) . (i,y) by A2, A1, A3, A5, FUNCT_5:31 .= (uncurry f) . (y,i) by A6, FUNCT_4:43 .= (f . y) . i by A7, A10, A9, FUNCT_5:def_2 ; hence x in pi ((f .: A),i) by A8, CARD_3:def_6; ::_thesis: verum end; end; theorem Th7: :: WAYBEL27:7 for f being Function-yielding Function for i, A being set st ( for g being Function st g in f .: A holds i in dom g ) holds pi ((f .: A),i) c= ((commute f) . i) .: A proof let f be Function-yielding Function; ::_thesis: for i, A being set st ( for g being Function st g in f .: A holds i in dom g ) holds pi ((f .: A),i) c= ((commute f) . i) .: A let i, A be set ; ::_thesis: ( ( for g being Function st g in f .: A holds i in dom g ) implies pi ((f .: A),i) c= ((commute f) . i) .: A ) assume A1: for g being Function st g in f .: A holds i in dom g ; ::_thesis: pi ((f .: A),i) c= ((commute f) . i) .: A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in pi ((f .: A),i) or x in ((commute f) . i) .: A ) assume x in pi ((f .: A),i) ; ::_thesis: x in ((commute f) . i) .: A then consider g being Function such that A2: g in f .: A and A3: x = g . i by CARD_3:def_6; consider y being set such that A4: y in dom f and A5: y in A and A6: g = f . y by A2, FUNCT_1:def_6; i in dom g by A1, A2; then A7: [y,i] in dom (uncurry f) by A4, A6, FUNCT_5:def_2; then A8: [i,y] in dom (~ (uncurry f)) by FUNCT_4:def_2; then A9: i in proj1 (dom (~ (uncurry f))) by XTUPLE_0:def_12; then A10: i in dom (curry (~ (uncurry f))) by FUNCT_5:def_1; A11: i in {i} by TARSKI:def_1; y in proj2 (dom (~ (uncurry f))) by A8, XTUPLE_0:def_13; then [i,y] in [:{i},(proj2 (dom (~ (uncurry f)))):] by A11, ZFMISC_1:87; then A12: [i,y] in (dom (~ (uncurry f))) /\ [:{i},(proj2 (dom (~ (uncurry f)))):] by A8, XBOOLE_0:def_4; then A13: y in proj2 ((dom (~ (uncurry f))) /\ [:{i},(proj2 (dom (~ (uncurry f)))):]) by XTUPLE_0:def_13; A14: [y,i] `2 = i ; A15: [y,i] `1 = y ; A16: commute f = curry' (uncurry f) by FUNCT_6:def_10 .= curry (~ (uncurry f)) by FUNCT_5:def_3 ; A17: ex h being Function st ( (curry (~ (uncurry f))) . i = h & dom h = proj2 ((dom (~ (uncurry f))) /\ [:{i},(proj2 (dom (~ (uncurry f)))):]) & ( for b being set st b in dom h holds h . b = (~ (uncurry f)) . (i,b) ) ) by A9, FUNCT_5:def_1; then y in dom ((commute f) . i) by A16, A12, XTUPLE_0:def_13; then ((commute f) . i) . y = (~ (uncurry f)) . (i,y) by A16, A10, FUNCT_5:31 .= (uncurry f) . (y,i) by A7, FUNCT_4:def_2 .= x by A3, A6, A7, A15, A14, FUNCT_5:def_2 ; hence x in ((commute f) . i) .: A by A5, A16, A17, A13, FUNCT_1:def_6; ::_thesis: verum end; theorem Th8: :: WAYBEL27:8 for X, Y being set for f being Function st rng f c= Funcs (X,Y) holds for i, A being set st i in X holds ((commute f) . i) .: A = pi ((f .: A),i) proof let X, Y be set ; ::_thesis: for f being Function st rng f c= Funcs (X,Y) holds for i, A being set st i in X holds ((commute f) . i) .: A = pi ((f .: A),i) let f be Function; ::_thesis: ( rng f c= Funcs (X,Y) implies for i, A being set st i in X holds ((commute f) . i) .: A = pi ((f .: A),i) ) assume A1: rng f c= Funcs (X,Y) ; ::_thesis: for i, A being set st i in X holds ((commute f) . i) .: A = pi ((f .: A),i) then A2: f in Funcs ((dom f),(Funcs (X,Y))) by FUNCT_2:def_2; A3: f is Function-yielding proof let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 f or f . x is set ) assume x in dom f ; ::_thesis: f . x is set then f . x in rng f by FUNCT_1:def_3; hence f . x is set by A1; ::_thesis: verum end; let i, A be set ; ::_thesis: ( i in X implies ((commute f) . i) .: A = pi ((f .: A),i) ) assume A4: i in X ; ::_thesis: ((commute f) . i) .: A = pi ((f .: A),i) percases ( dom f = {} or dom f <> {} ) ; suppose dom f = {} ; ::_thesis: ((commute f) . i) .: A = pi ((f .: A),i) then A5: f = {} ; then (commute f) . i = {} by FUNCT_6:58; then A6: ((commute f) . i) .: A = {} ; f .: A = {} by A5; hence ((commute f) . i) .: A = pi ((f .: A),i) by A6, CARD_3:13; ::_thesis: verum end; suppose dom f <> {} ; ::_thesis: ((commute f) . i) .: A = pi ((f .: A),i) then commute f in Funcs (X,(Funcs ((dom f),Y))) by A2, A4, FUNCT_6:55; then ex g being Function st ( commute f = g & dom g = X & rng g c= Funcs ((dom f),Y) ) by FUNCT_2:def_2; hence ((commute f) . i) .: A c= pi ((f .: A),i) by A3, A4, Th6; :: according to XBOOLE_0:def_10 ::_thesis: pi ((f .: A),i) c= ((commute f) . i) .: A now__::_thesis:_for_g_being_Function_st_g_in_f_.:_A_holds_ i_in_dom_g let g be Function; ::_thesis: ( g in f .: A implies i in dom g ) A7: f .: A c= rng f by RELAT_1:111; assume g in f .: A ; ::_thesis: i in dom g then g in rng f by A7; then ex h being Function st ( g = h & dom h = X & rng h c= Y ) by A1, FUNCT_2:def_2; hence i in dom g by A4; ::_thesis: verum end; hence pi ((f .: A),i) c= ((commute f) . i) .: A by A3, Th7; ::_thesis: verum end; end; end; theorem Th9: :: WAYBEL27:9 for f being Function for i, A being set st [:A,{i}:] c= dom f holds pi (((curry f) .: A),i) = f .: [:A,{i}:] proof let f be Function; ::_thesis: for i, A being set st [:A,{i}:] c= dom f holds pi (((curry f) .: A),i) = f .: [:A,{i}:] let i, A be set ; ::_thesis: ( [:A,{i}:] c= dom f implies pi (((curry f) .: A),i) = f .: [:A,{i}:] ) assume A1: [:A,{i}:] c= dom f ; ::_thesis: pi (((curry f) .: A),i) = f .: [:A,{i}:] A2: i in {i} by TARSKI:def_1; thus pi (((curry f) .: A),i) c= f .: [:A,{i}:] :: according to XBOOLE_0:def_10 ::_thesis: f .: [:A,{i}:] c= pi (((curry f) .: A),i) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in pi (((curry f) .: A),i) or x in f .: [:A,{i}:] ) assume x in pi (((curry f) .: A),i) ; ::_thesis: x in f .: [:A,{i}:] then consider g being Function such that A3: g in (curry f) .: A and A4: x = g . i by CARD_3:def_6; consider a being set such that a in dom (curry f) and A5: a in A and A6: g = (curry f) . a by A3, FUNCT_1:def_6; A7: [a,i] in [:A,{i}:] by A2, A5, ZFMISC_1:def_2; then f . (a,i) in f .: [:A,{i}:] by A1, FUNCT_1:def_6; hence x in f .: [:A,{i}:] by A1, A4, A6, A7, FUNCT_5:20; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: [:A,{i}:] or x in pi (((curry f) .: A),i) ) assume x in f .: [:A,{i}:] ; ::_thesis: x in pi (((curry f) .: A),i) then consider y being set such that A8: y in dom f and A9: y in [:A,{i}:] and A10: x = f . y by FUNCT_1:def_6; consider y1, y2 being set such that A11: y1 in A and A12: y2 in {i} and A13: y = [y1,y2] by A9, ZFMISC_1:def_2; reconsider g = (curry f) . y1 as Function by A8, A13, FUNCT_5:19; y1 in dom (curry f) by A8, A13, FUNCT_5:19; then A14: g in (curry f) .: A by A11, FUNCT_1:def_6; A15: y2 = i by A12, TARSKI:def_1; x = f . (y1,y2) by A10, A13; then x = g . i by A15, A8, A13, FUNCT_5:20; hence x in pi (((curry f) .: A),i) by A14, CARD_3:def_6; ::_thesis: verum end; registration let T be constituted-Functions 1-sorted ; cluster the carrier of T -> functional ; coherence the carrier of T is functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in the carrier of T or x is set ) assume x in the carrier of T ; ::_thesis: x is set hence x is set ; ::_thesis: verum end; end; registration cluster non empty constituted-Functions strict reflexive transitive antisymmetric V219() V220() complete non void for RelStr ; existence ex b1 being LATTICE st ( b1 is constituted-Functions & b1 is complete & b1 is strict ) proof set L = the complete LATTICE; take the complete LATTICE |^ {} ; ::_thesis: ( the complete LATTICE |^ {} is constituted-Functions & the complete LATTICE |^ {} is complete & the complete LATTICE |^ {} is strict ) thus ( the complete LATTICE |^ {} is constituted-Functions & the complete LATTICE |^ {} is complete & the complete LATTICE |^ {} is strict ) ; ::_thesis: verum end; cluster non empty constituted-Functions for 1-sorted ; existence ex b1 being 1-sorted st ( b1 is constituted-Functions & not b1 is empty ) proof set L = the complete LATTICE; take the complete LATTICE |^ {} ; ::_thesis: ( the complete LATTICE |^ {} is constituted-Functions & not the complete LATTICE |^ {} is empty ) thus ( the complete LATTICE |^ {} is constituted-Functions & not the complete LATTICE |^ {} is empty ) ; ::_thesis: verum end; end; registration let T be non empty constituted-Functions RelStr ; cluster non empty -> non empty constituted-Functions for SubRelStr of T; coherence for b1 being non empty SubRelStr of T holds b1 is constituted-Functions proof let S be non empty SubRelStr of T; ::_thesis: S is constituted-Functions let a be Element of S; :: according to MONOID_0:def_1 ::_thesis: a is set the carrier of S c= the carrier of T by YELLOW_0:def_13; hence a is set ; ::_thesis: verum end; end; theorem Th10: :: WAYBEL27:10 for S, T being complete LATTICE for f being idempotent Function of T,T for h being Function of S,(Image f) holds f * h = h proof let S, T be complete LATTICE; ::_thesis: for f being idempotent Function of T,T for h being Function of S,(Image f) holds f * h = h let f be idempotent Function of T,T; ::_thesis: for h being Function of S,(Image f) holds f * h = h let h be Function of S,(Image f); ::_thesis: f * h = h rng h c= the carrier of (Image f) ; then A1: rng h c= rng f by YELLOW_0:def_15; f * f = f by QUANTAL1:def_9; then rng f c= dom f by FUNCT_1:15; then rng h c= dom f by A1, XBOOLE_1:1; hence f * h = h by A1, YELLOW16:4; ::_thesis: verum end; theorem :: WAYBEL27:11 for S, T, T1 being non empty RelStr st T is SubRelStr of T1 holds for f being Function of S,T for f1 being Function of S,T1 st f is monotone & f = f1 holds f1 is monotone proof let S be non empty RelStr ; ::_thesis: for T, T1 being non empty RelStr st T is SubRelStr of T1 holds for f being Function of S,T for f1 being Function of S,T1 st f is monotone & f = f1 holds f1 is monotone let T, T1 be non empty RelStr ; ::_thesis: ( T is SubRelStr of T1 implies for f being Function of S,T for f1 being Function of S,T1 st f is monotone & f = f1 holds f1 is monotone ) assume A1: T is SubRelStr of T1 ; ::_thesis: for f being Function of S,T for f1 being Function of S,T1 st f is monotone & f = f1 holds f1 is monotone let f be Function of S,T; ::_thesis: for f1 being Function of S,T1 st f is monotone & f = f1 holds f1 is monotone let f1 be Function of S,T1; ::_thesis: ( f is monotone & f = f1 implies f1 is monotone ) assume that A2: f is monotone and A3: f = f1 ; ::_thesis: f1 is monotone thus f1 is monotone ::_thesis: verum proof let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f1 . x <= f1 . y ) assume x <= y ; ::_thesis: f1 . x <= f1 . y then f . x <= f . y by A2, WAYBEL_1:def_2; hence f1 . x <= f1 . y by A1, A3, YELLOW_0:59; ::_thesis: verum end; end; theorem Th12: :: WAYBEL27:12 for S, T, T1 being non empty RelStr st T is full SubRelStr of T1 holds for f being Function of S,T for f1 being Function of S,T1 st f1 is monotone & f = f1 holds f is monotone proof let S be non empty RelStr ; ::_thesis: for T, T1 being non empty RelStr st T is full SubRelStr of T1 holds for f being Function of S,T for f1 being Function of S,T1 st f1 is monotone & f = f1 holds f is monotone let T, T1 be non empty RelStr ; ::_thesis: ( T is full SubRelStr of T1 implies for f being Function of S,T for f1 being Function of S,T1 st f1 is monotone & f = f1 holds f is monotone ) assume A1: T is full SubRelStr of T1 ; ::_thesis: for f being Function of S,T for f1 being Function of S,T1 st f1 is monotone & f = f1 holds f is monotone let f be Function of S,T; ::_thesis: for f1 being Function of S,T1 st f1 is monotone & f = f1 holds f is monotone let f1 be Function of S,T1; ::_thesis: ( f1 is monotone & f = f1 implies f is monotone ) assume that A2: f1 is monotone and A3: f = f1 ; ::_thesis: f is monotone thus f is monotone ::_thesis: verum proof let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume x <= y ; ::_thesis: f . x <= f . y then f1 . x <= f1 . y by A2, WAYBEL_1:def_2; hence f . x <= f . y by A1, A3, YELLOW_0:60; ::_thesis: verum end; end; theorem Th13: :: WAYBEL27:13 for X being set for V being Subset of X holds ( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V ) proof let X be set ; ::_thesis: for V being Subset of X holds ( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V ) let V be Subset of X; ::_thesis: ( (chi (V,X)) " {1} = V & (chi (V,X)) " {0} = X \ V ) thus (chi (V,X)) " {1} = V ::_thesis: (chi (V,X)) " {0} = X \ V proof thus (chi (V,X)) " {1} c= V :: according to XBOOLE_0:def_10 ::_thesis: V c= (chi (V,X)) " {1} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (chi (V,X)) " {1} or x in V ) assume A1: x in (chi (V,X)) " {1} ; ::_thesis: x in V then (chi (V,X)) . x in {1} by FUNCT_1:def_7; then (chi (V,X)) . x = 1 by TARSKI:def_1; hence x in V by A1, FUNCT_3:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in (chi (V,X)) " {1} ) assume A2: x in V ; ::_thesis: x in (chi (V,X)) " {1} then (chi (V,X)) . x = 1 by FUNCT_3:def_3; then A3: (chi (V,X)) . x in {1} by TARSKI:def_1; x in X by A2; then x in dom (chi (V,X)) by FUNCT_3:def_3; hence x in (chi (V,X)) " {1} by A3, FUNCT_1:def_7; ::_thesis: verum end; thus (chi (V,X)) " {0} = X \ V ::_thesis: verum proof thus (chi (V,X)) " {0} c= X \ V :: according to XBOOLE_0:def_10 ::_thesis: X \ V c= (chi (V,X)) " {0} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (chi (V,X)) " {0} or x in X \ V ) A4: ( x in V implies (chi (V,X)) . x = 1 ) by FUNCT_3:def_3; assume A5: x in (chi (V,X)) " {0} ; ::_thesis: x in X \ V then (chi (V,X)) . x in {0} by FUNCT_1:def_7; hence x in X \ V by A4, A5, TARSKI:def_1, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ V or x in (chi (V,X)) " {0} ) assume A6: x in X \ V ; ::_thesis: x in (chi (V,X)) " {0} then not x in V by XBOOLE_0:def_5; then (chi (V,X)) . x = 0 by A6, FUNCT_3:def_3; then A7: (chi (V,X)) . x in {0} by TARSKI:def_1; x in X by A6; then x in dom (chi (V,X)) by FUNCT_3:def_3; hence x in (chi (V,X)) " {0} by A7, FUNCT_1:def_7; ::_thesis: verum end; end; begin definition let X be non empty set ; let T be non empty RelStr ; let f be Element of (T |^ X); let x be Element of X; :: original: . redefine funcf . x -> Element of T; coherence f . x is Element of T proof reconsider p = f as Element of (product (X --> T)) by YELLOW_1:def_5; p . x is Element of ((X --> T) . x) ; hence f . x is Element of T by FUNCOP_1:7; ::_thesis: verum end; end; theorem Th14: :: WAYBEL27:14 for X being non empty set for T being non empty RelStr for f, g being Element of (T |^ X) holds ( f <= g iff for x being Element of X holds f . x <= g . x ) proof let X be non empty set ; ::_thesis: for T being non empty RelStr for f, g being Element of (T |^ X) holds ( f <= g iff for x being Element of X holds f . x <= g . x ) let T be non empty RelStr ; ::_thesis: for f, g being Element of (T |^ X) holds ( f <= g iff for x being Element of X holds f . x <= g . x ) let f, g be Element of (T |^ X); ::_thesis: ( f <= g iff for x being Element of X holds f . x <= g . x ) reconsider a = f, b = g as Element of (product (X --> T)) by YELLOW_1:def_5; A1: T |^ X = product (X --> T) by YELLOW_1:def_5; hereby ::_thesis: ( ( for x being Element of X holds f . x <= g . x ) implies f <= g ) assume A2: f <= g ; ::_thesis: for x being Element of X holds f . x <= g . x let x be Element of X; ::_thesis: f . x <= g . x (X --> T) . x = T by FUNCOP_1:7; hence f . x <= g . x by A1, A2, WAYBEL_3:28; ::_thesis: verum end; assume A3: for x being Element of X holds f . x <= g . x ; ::_thesis: f <= g now__::_thesis:_for_x_being_Element_of_X_holds_a_._x_<=_b_._x let x be Element of X; ::_thesis: a . x <= b . x (X --> T) . x = T by FUNCOP_1:7; hence a . x <= b . x by A3; ::_thesis: verum end; hence f <= g by A1, WAYBEL_3:28; ::_thesis: verum end; theorem Th15: :: WAYBEL27:15 for X being set for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds L |^ X = S |^ X proof let X be set ; ::_thesis: for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds L |^ X = S |^ X let L, S be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) implies L |^ X = S |^ X ) assume A1: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) ; ::_thesis: L |^ X = S |^ X reconsider tXL = X --> L as RelStr-yielding ManySortedSet of X ; reconsider tXS = X --> S as RelStr-yielding ManySortedSet of X ; A2: for x being set st x in dom (Carrier tXS) holds (Carrier tXS) . x = (Carrier tXL) . x proof let x be set ; ::_thesis: ( x in dom (Carrier tXS) implies (Carrier tXS) . x = (Carrier tXL) . x ) assume x in dom (Carrier tXS) ; ::_thesis: (Carrier tXS) . x = (Carrier tXL) . x then A3: x in X ; then A4: ex R1 being 1-sorted st ( tXL . x = R1 & (Carrier tXL) . x = the carrier of R1 ) by PRALG_1:def_13; ex R being 1-sorted st ( tXS . x = R & (Carrier tXS) . x = the carrier of R ) by A3, PRALG_1:def_13; hence (Carrier tXS) . x = the carrier of S by A3, FUNCOP_1:7 .= (Carrier tXL) . x by A1, A3, A4, FUNCOP_1:7 ; ::_thesis: verum end; A5: dom (Carrier tXS) = X by PARTFUN1:def_2 .= dom (Carrier tXL) by PARTFUN1:def_2 ; A6: the carrier of (S |^ X) = the carrier of (product tXS) by YELLOW_1:def_5 .= product (Carrier tXS) by YELLOW_1:def_4 .= product (Carrier tXL) by A5, A2, FUNCT_1:2 .= the carrier of (product tXL) by YELLOW_1:def_4 .= the carrier of (L |^ X) by YELLOW_1:def_5 ; A7: the InternalRel of (L |^ X) c= the InternalRel of (S |^ X) proof reconsider tXS = X --> S as RelStr-yielding ManySortedSet of X ; reconsider tXL = X --> L as RelStr-yielding ManySortedSet of X ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of (L |^ X) or x in the InternalRel of (S |^ X) ) assume A8: x in the InternalRel of (L |^ X) ; ::_thesis: x in the InternalRel of (S |^ X) then consider a, b being set such that A9: x = [a,b] and A10: a in the carrier of (L |^ X) and A11: b in the carrier of (L |^ X) by RELSET_1:2; reconsider a = a, b = b as Element of (L |^ X) by A10, A11; A12: L |^ X = product tXL by YELLOW_1:def_5; then A13: the carrier of (L |^ X) = product (Carrier tXL) by YELLOW_1:def_4; a <= b by A8, A9, ORDERS_2:def_5; then consider f, g being Function such that A14: f = a and A15: g = b and A16: for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) by A12, A13, YELLOW_1:def_4; reconsider a1 = a, b1 = b as Element of (S |^ X) by A6; A17: ex f, g being Function st ( f = a1 & g = b1 & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) ) ) proof take f ; ::_thesis: ex g being Function st ( f = a1 & g = b1 & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) ) ) take g ; ::_thesis: ( f = a1 & g = b1 & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) ) ) thus ( f = a1 & g = b1 ) by A14, A15; ::_thesis: for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) ) assume A18: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) then consider R being RelStr , xi, yi being Element of R such that A19: R = tXL . i and A20: xi = f . i and A21: yi = g . i and A22: xi <= yi by A16; take R1 = S; ::_thesis: ex xi, yi being Element of R1 st ( R1 = tXS . i & xi = f . i & yi = g . i & xi <= yi ) reconsider xi1 = xi, yi1 = yi as Element of R1 by A1, A18, A19, FUNCOP_1:7; take xi1 ; ::_thesis: ex yi being Element of R1 st ( R1 = tXS . i & xi1 = f . i & yi = g . i & xi1 <= yi ) take yi1 ; ::_thesis: ( R1 = tXS . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) thus R1 = tXS . i by A18, FUNCOP_1:7; ::_thesis: ( xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) thus ( xi1 = f . i & yi1 = g . i ) by A20, A21; ::_thesis: xi1 <= yi1 the InternalRel of R = the InternalRel of L by A18, A19, FUNCOP_1:7; then [xi1,yi1] in the InternalRel of R1 by A1, A22, ORDERS_2:def_5; hence xi1 <= yi1 by ORDERS_2:def_5; ::_thesis: verum end; A23: S |^ X = product tXS by YELLOW_1:def_5; then the carrier of (S |^ X) = product (Carrier tXS) by YELLOW_1:def_4; then a1 <= b1 by A17, A23, YELLOW_1:def_4; hence x in the InternalRel of (S |^ X) by A9, ORDERS_2:def_5; ::_thesis: verum end; the InternalRel of (S |^ X) c= the InternalRel of (L |^ X) proof reconsider tXL = X --> L as RelStr-yielding ManySortedSet of X ; reconsider tXS = X --> S as RelStr-yielding ManySortedSet of X ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the InternalRel of (S |^ X) or x in the InternalRel of (L |^ X) ) assume A24: x in the InternalRel of (S |^ X) ; ::_thesis: x in the InternalRel of (L |^ X) then consider a, b being set such that A25: x = [a,b] and A26: a in the carrier of (S |^ X) and A27: b in the carrier of (S |^ X) by RELSET_1:2; reconsider a = a, b = b as Element of (S |^ X) by A26, A27; A28: S |^ X = product tXS by YELLOW_1:def_5; then A29: the carrier of (S |^ X) = product (Carrier tXS) by YELLOW_1:def_4; a <= b by A24, A25, ORDERS_2:def_5; then consider f, g being Function such that A30: f = a and A31: g = b and A32: for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXS . i & xi = f . i & yi = g . i & xi <= yi ) by A28, A29, YELLOW_1:def_4; reconsider a1 = a, b1 = b as Element of (L |^ X) by A6; A33: ex f, g being Function st ( f = a1 & g = b1 & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) ) ) proof take f ; ::_thesis: ex g being Function st ( f = a1 & g = b1 & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) ) ) take g ; ::_thesis: ( f = a1 & g = b1 & ( for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) ) ) thus ( f = a1 & g = b1 ) by A30, A31; ::_thesis: for i being set st i in X holds ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) let i be set ; ::_thesis: ( i in X implies ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) ) assume A34: i in X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st ( R = tXL . i & xi = f . i & yi = g . i & xi <= yi ) then consider R being RelStr , xi, yi being Element of R such that A35: R = tXS . i and A36: xi = f . i and A37: yi = g . i and A38: xi <= yi by A32; take R1 = L; ::_thesis: ex xi, yi being Element of R1 st ( R1 = tXL . i & xi = f . i & yi = g . i & xi <= yi ) reconsider xi1 = xi, yi1 = yi as Element of R1 by A1, A34, A35, FUNCOP_1:7; take xi1 ; ::_thesis: ex yi being Element of R1 st ( R1 = tXL . i & xi1 = f . i & yi = g . i & xi1 <= yi ) take yi1 ; ::_thesis: ( R1 = tXL . i & xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) thus R1 = tXL . i by A34, FUNCOP_1:7; ::_thesis: ( xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) thus ( xi1 = f . i & yi1 = g . i ) by A36, A37; ::_thesis: xi1 <= yi1 the InternalRel of R = the InternalRel of S by A34, A35, FUNCOP_1:7; then [xi1,yi1] in the InternalRel of R1 by A1, A38, ORDERS_2:def_5; hence xi1 <= yi1 by ORDERS_2:def_5; ::_thesis: verum end; A39: L |^ X = product tXL by YELLOW_1:def_5; then the carrier of (L |^ X) = product (Carrier tXL) by YELLOW_1:def_4; then a1 <= b1 by A33, A39, YELLOW_1:def_4; hence x in the InternalRel of (L |^ X) by A25, ORDERS_2:def_5; ::_thesis: verum end; hence L |^ X = S |^ X by A7, A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: WAYBEL27:16 for S1, S2, T1, T2 being non empty TopSpace st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds oContMaps (S1,T1) = oContMaps (S2,T2) proof let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies oContMaps (S1,T1) = oContMaps (S2,T2) ) assume that A1: TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) and A2: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: oContMaps (S1,T1) = oContMaps (S2,T2) A3: oContMaps (S2,T2) = ContMaps (S2,(Omega T2)) by WAYBEL26:def_1; Omega T1 = Omega T2 by A2, WAYBEL25:13; then reconsider oCM2 = oContMaps (S2,T2) as full SubRelStr of (Omega T1) |^ the carrier of S1 by A3, A1, WAYBEL24:def_3; oContMaps (S1,T1) = ContMaps (S1,(Omega T1)) by WAYBEL26:def_1; then reconsider oCM1 = oContMaps (S1,T1) as full SubRelStr of (Omega T1) |^ the carrier of S1 by WAYBEL24:def_3; the carrier of oCM1 = the carrier of oCM2 proof thus the carrier of oCM1 c= the carrier of oCM2 :: according to XBOOLE_0:def_10 ::_thesis: the carrier of oCM2 c= the carrier of oCM1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of oCM1 or x in the carrier of oCM2 ) A4: TopStruct(# the carrier of (Omega T2), the topology of (Omega T2) #) = TopStruct(# the carrier of T2, the topology of T2 #) by WAYBEL25:def_2; assume x in the carrier of oCM1 ; ::_thesis: x in the carrier of oCM2 then x in the carrier of (ContMaps (S1,(Omega T1))) by WAYBEL26:def_1; then consider f being Function of S1,(Omega T1) such that A5: x = f and A6: f is continuous by WAYBEL24:def_3; A7: TopStruct(# the carrier of (Omega T1), the topology of (Omega T1) #) = TopStruct(# the carrier of T1, the topology of T1 #) by WAYBEL25:def_2; then reconsider f1 = f as Function of S2,(Omega T2) by A4, A1, A2; for P1 being Subset of (Omega T2) st P1 is closed holds f1 " P1 is closed proof let P1 be Subset of (Omega T2); ::_thesis: ( P1 is closed implies f1 " P1 is closed ) reconsider P = P1 as Subset of (Omega T1) by A2, A7, A4; assume P1 is closed ; ::_thesis: f1 " P1 is closed then P is closed by A2, A7, A4, TOPS_3:79; then f " P is closed by A6, PRE_TOPC:def_6; hence f1 " P1 is closed by A1, TOPS_3:79; ::_thesis: verum end; then f1 is continuous by PRE_TOPC:def_6; then x in the carrier of (ContMaps (S2,(Omega T2))) by A5, WAYBEL24:def_3; hence x in the carrier of oCM2 by WAYBEL26:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of oCM2 or x in the carrier of oCM1 ) A8: TopStruct(# the carrier of (Omega T1), the topology of (Omega T1) #) = TopStruct(# the carrier of T1, the topology of T1 #) by WAYBEL25:def_2; assume x in the carrier of oCM2 ; ::_thesis: x in the carrier of oCM1 then x in the carrier of (ContMaps (S2,(Omega T2))) by WAYBEL26:def_1; then consider f being Function of S2,(Omega T2) such that A9: x = f and A10: f is continuous by WAYBEL24:def_3; A11: TopStruct(# the carrier of (Omega T2), the topology of (Omega T2) #) = TopStruct(# the carrier of T2, the topology of T2 #) by WAYBEL25:def_2; then reconsider f1 = f as Function of S1,(Omega T1) by A8, A1, A2; for P1 being Subset of (Omega T1) st P1 is closed holds f1 " P1 is closed proof let P1 be Subset of (Omega T1); ::_thesis: ( P1 is closed implies f1 " P1 is closed ) reconsider P = P1 as Subset of (Omega T2) by A2, A11, A8; assume P1 is closed ; ::_thesis: f1 " P1 is closed then P is closed by A2, A11, A8, TOPS_3:79; then f " P is closed by A10, PRE_TOPC:def_6; hence f1 " P1 is closed by A1, TOPS_3:79; ::_thesis: verum end; then f1 is continuous by PRE_TOPC:def_6; then x in the carrier of (ContMaps (S1,(Omega T1))) by A9, WAYBEL24:def_3; hence x in the carrier of oCM1 by WAYBEL26:def_1; ::_thesis: verum end; hence oContMaps (S1,T1) = oContMaps (S2,T2) by YELLOW_0:57; ::_thesis: verum end; theorem Th17: :: WAYBEL27:17 for X being set ex f being Function of (BoolePoset X),((BoolePoset 1) |^ X) st ( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) ) proof let Z be set ; ::_thesis: ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) ) percases ( Z = {} or Z <> {} ) ; supposeA1: Z = {} ; ::_thesis: ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) ) then A2: (BoolePoset 1) |^ Z = RelStr(# {{}},(id {{}}) #) by YELLOW_1:27; A3: InclPoset (bool {}) = RelStr(# (bool {}),(RelIncl (bool {})) #) by YELLOW_1:def_1; A4: BoolePoset Z = InclPoset (bool {}) by A1, YELLOW_1:4; then reconsider f = id {{}} as Function of (BoolePoset Z),((BoolePoset 1) |^ Z) by A3, A1, YELLOW_1:27, ZFMISC_1:1; take f ; ::_thesis: ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) ) A5: rng (id {{}}) = {{}} ; for x, y being Element of (BoolePoset Z) holds ( x <= y iff f . x <= f . y ) by A4, A3; hence f is isomorphic by A2, A5, WAYBEL_0:66; ::_thesis: for Y being Subset of Z holds f . Y = chi (Y,Z) let Y be Subset of Z; ::_thesis: f . Y = chi (Y,Z) Y = {} by A1; then Y in {{}} by TARSKI:def_1; then f . Y = {} by A1, FUNCT_1:18; hence f . Y = chi (Y,Z) by A1; ::_thesis: verum end; suppose Z <> {} ; ::_thesis: ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) ) then reconsider Z9 = Z as non empty set ; (BoolePoset 1) |^ Z = product (Z9 --> (BoolePoset 1)) by YELLOW_1:def_5; hence ex f being Function of (BoolePoset Z),((BoolePoset 1) |^ Z) st ( f is isomorphic & ( for Y being Subset of Z holds f . Y = chi (Y,Z) ) ) by WAYBEL18:14; ::_thesis: verum end; end; end; theorem Th18: :: WAYBEL27:18 for X being set holds BoolePoset X,(BoolePoset 1) |^ X are_isomorphic proof let X be set ; ::_thesis: BoolePoset X,(BoolePoset 1) |^ X are_isomorphic consider f being Function of (BoolePoset X),((BoolePoset 1) |^ X) such that A1: f is isomorphic and for Y being Subset of X holds f . Y = chi (Y,X) by Th17; take f ; :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic thus f is isomorphic by A1; ::_thesis: verum end; theorem Th19: :: WAYBEL27:19 for X, Y being non empty set for T being non empty Poset for S1 being non empty full SubRelStr of (T |^ X) |^ Y for S2 being non empty full SubRelStr of (T |^ Y) |^ X for F being Function of S1,S2 st F is commuting holds F is monotone proof let X, Y be non empty set ; ::_thesis: for T being non empty Poset for S1 being non empty full SubRelStr of (T |^ X) |^ Y for S2 being non empty full SubRelStr of (T |^ Y) |^ X for F being Function of S1,S2 st F is commuting holds F is monotone let T be non empty Poset; ::_thesis: for S1 being non empty full SubRelStr of (T |^ X) |^ Y for S2 being non empty full SubRelStr of (T |^ Y) |^ X for F being Function of S1,S2 st F is commuting holds F is monotone let S1 be non empty full SubRelStr of (T |^ X) |^ Y; ::_thesis: for S2 being non empty full SubRelStr of (T |^ Y) |^ X for F being Function of S1,S2 st F is commuting holds F is monotone let S2 be non empty full SubRelStr of (T |^ Y) |^ X; ::_thesis: for F being Function of S1,S2 st F is commuting holds F is monotone let F be Function of S1,S2; ::_thesis: ( F is commuting implies F is monotone ) assume that for x being set st x in dom F holds x is Function-yielding Function and A1: for f being Function st f in dom F holds F . f = commute f ; :: according to WAYBEL27:def_3 ::_thesis: F is monotone let f, g be Element of S1; :: according to WAYBEL_1:def_2 ::_thesis: ( not f <= g or F . f <= F . g ) A2: dom F = the carrier of S1 by FUNCT_2:def_1; then A3: F . g = commute g by A1; reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) by YELLOW_0:58; reconsider a = f, b = g as Element of ((T |^ X) |^ Y) by YELLOW_0:58; A4: the carrier of ((T |^ X) |^ Y) = Funcs (Y, the carrier of (T |^ X)) by YELLOW_1:28 .= Funcs (Y,(Funcs (X, the carrier of T))) by YELLOW_1:28 ; assume f <= g ; ::_thesis: F . f <= F . g then A5: a <= b by YELLOW_0:59; A6: F . f = commute a by A2, A1; now__::_thesis:_for_x_being_Element_of_X_holds_Fa_._x_<=_Fb_._x let x be Element of X; ::_thesis: Fa . x <= Fb . x now__::_thesis:_for_y_being_Element_of_Y_holds_(Fa_._x)_._y_<=_(Fb_._x)_._y let y be Element of Y; ::_thesis: (Fa . x) . y <= (Fb . x) . y A7: (Fa . x) . y = (a . y) . x by A4, A6, FUNCT_6:56; A8: (Fb . x) . y = (b . y) . x by A4, A3, FUNCT_6:56; a . y <= b . y by A5, Th14; hence (Fa . x) . y <= (Fb . x) . y by A7, A8, Th14; ::_thesis: verum end; hence Fa . x <= Fb . x by Th14; ::_thesis: verum end; then Fa <= Fb by Th14; hence F . f <= F . g by YELLOW_0:60; ::_thesis: verum end; theorem Th20: :: WAYBEL27:20 for X, Y being non empty set for T being non empty Poset for S1 being non empty full SubRelStr of (T |^ Y) |^ X for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S1,S2 st F is uncurrying holds F is monotone proof let X, Y be non empty set ; ::_thesis: for T being non empty Poset for S1 being non empty full SubRelStr of (T |^ Y) |^ X for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S1,S2 st F is uncurrying holds F is monotone let T be non empty Poset; ::_thesis: for S1 being non empty full SubRelStr of (T |^ Y) |^ X for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S1,S2 st F is uncurrying holds F is monotone let S1 be non empty full SubRelStr of (T |^ Y) |^ X; ::_thesis: for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S1,S2 st F is uncurrying holds F is monotone let S2 be non empty full SubRelStr of T |^ [:X,Y:]; ::_thesis: for F being Function of S1,S2 st F is uncurrying holds F is monotone let F be Function of S1,S2; ::_thesis: ( F is uncurrying implies F is monotone ) assume that for x being set st x in dom F holds x is Function-yielding Function and A1: for f being Function st f in dom F holds F . f = uncurry f ; :: according to WAYBEL27:def_1 ::_thesis: F is monotone let f, g be Element of S1; :: according to WAYBEL_1:def_2 ::_thesis: ( not f <= g or F . f <= F . g ) reconsider a = f, b = g as Element of ((T |^ Y) |^ X) by YELLOW_0:58; A2: dom F = the carrier of S1 by FUNCT_2:def_1; then A3: F . g = uncurry b by A1; reconsider Fa = F . f, Fb = F . g as Element of (T |^ [:X,Y:]) by YELLOW_0:58; assume f <= g ; ::_thesis: F . f <= F . g then A4: a <= b by YELLOW_0:59; A5: the carrier of (T |^ Y) = Funcs (Y, the carrier of T) by YELLOW_1:28; then A6: the carrier of ((T |^ Y) |^ X) = Funcs (X,(Funcs (Y, the carrier of T))) by YELLOW_1:28; A7: F . f = uncurry a by A2, A1; now__::_thesis:_for_xy_being_Element_of_[:X,Y:]_holds_Fa_._xy_<=_Fb_._xy let xy be Element of [:X,Y:]; ::_thesis: Fa . xy <= Fb . xy consider x, y being set such that A8: x in X and A9: y in Y and A10: xy = [x,y] by ZFMISC_1:def_2; reconsider y = y as Element of Y by A9; reconsider x = x as Element of X by A8; A11: a . x <= b . x by A4, Th14; b is Function of X,(Funcs (Y, the carrier of T)) by A6, FUNCT_2:66; then A12: dom b = X by FUNCT_2:def_1; a is Function of X,(Funcs (Y, the carrier of T)) by A6, FUNCT_2:66; then A13: dom a = X by FUNCT_2:def_1; b . x is Function of Y, the carrier of T by A5, FUNCT_2:66; then dom (b . x) = Y by FUNCT_2:def_1; then A14: Fb . (x,y) = (b . x) . y by A12, A3, FUNCT_5:38; a . x is Function of Y, the carrier of T by A5, FUNCT_2:66; then dom (a . x) = Y by FUNCT_2:def_1; then Fa . (x,y) = (a . x) . y by A13, A7, FUNCT_5:38; hence Fa . xy <= Fb . xy by A14, A11, A10, Th14; ::_thesis: verum end; then Fa <= Fb by Th14; hence F . f <= F . g by YELLOW_0:60; ::_thesis: verum end; theorem Th21: :: WAYBEL27:21 for X, Y being non empty set for T being non empty Poset for S1 being non empty full SubRelStr of (T |^ Y) |^ X for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S2,S1 st F is currying holds F is monotone proof let X, Y be non empty set ; ::_thesis: for T being non empty Poset for S1 being non empty full SubRelStr of (T |^ Y) |^ X for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S2,S1 st F is currying holds F is monotone let T be non empty Poset; ::_thesis: for S1 being non empty full SubRelStr of (T |^ Y) |^ X for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S2,S1 st F is currying holds F is monotone let S1 be non empty full SubRelStr of (T |^ Y) |^ X; ::_thesis: for S2 being non empty full SubRelStr of T |^ [:X,Y:] for F being Function of S2,S1 st F is currying holds F is monotone let S2 be non empty full SubRelStr of T |^ [:X,Y:]; ::_thesis: for F being Function of S2,S1 st F is currying holds F is monotone let F be Function of S2,S1; ::_thesis: ( F is currying implies F is monotone ) assume that for x being set st x in dom F holds ( x is Function & proj1 x is Relation ) and A1: for f being Function st f in dom F holds F . f = curry f ; :: according to WAYBEL27:def_2 ::_thesis: F is monotone let f, g be Element of S2; :: according to WAYBEL_1:def_2 ::_thesis: ( not f <= g or F . f <= F . g ) reconsider a = f, b = g as Element of (T |^ [:X,Y:]) by YELLOW_0:58; A2: dom F = the carrier of S2 by FUNCT_2:def_1; then A3: F . g = curry b by A1; reconsider Fa = F . f, Fb = F . g as Element of ((T |^ Y) |^ X) by YELLOW_0:58; assume f <= g ; ::_thesis: F . f <= F . g then A4: a <= b by YELLOW_0:59; A5: the carrier of (T |^ Y) = Funcs (Y, the carrier of T) by YELLOW_1:28; then A6: the carrier of ((T |^ Y) |^ X) = Funcs (X,(Funcs (Y, the carrier of T))) by YELLOW_1:28; A7: F . f = curry a by A2, A1; now__::_thesis:_for_x_being_Element_of_X_holds_Fa_._x_<=_Fb_._x let x be Element of X; ::_thesis: Fa . x <= Fb . x now__::_thesis:_for_y_being_Element_of_Y_holds_(Fa_._x)_._y_<=_(Fb_._x)_._y let y be Element of Y; ::_thesis: (Fa . x) . y <= (Fb . x) . y reconsider xy = [x,y] as Element of [:X,Y:] ; Fa . x is Function of Y, the carrier of T by A5, FUNCT_2:66; then A8: dom (Fa . x) = Y by FUNCT_2:def_1; Fa is Function of X,(Funcs (Y, the carrier of T)) by A6, FUNCT_2:66; then dom Fa = X by FUNCT_2:def_1; then (Fa . x) . y = a . (x,y) by A8, A7, FUNCT_5:31; then A9: (Fa . x) . y = a . xy ; Fb . x is Function of Y, the carrier of T by A5, FUNCT_2:66; then A10: dom (Fb . x) = Y by FUNCT_2:def_1; Fb is Function of X,(Funcs (Y, the carrier of T)) by A6, FUNCT_2:66; then dom Fb = X by FUNCT_2:def_1; then (Fb . x) . y = b . (x,y) by A10, A3, FUNCT_5:31; hence (Fa . x) . y <= (Fb . x) . y by A9, A4, Th14; ::_thesis: verum end; hence Fa . x <= Fb . x by Th14; ::_thesis: verum end; then Fa <= Fb by Th14; hence F . f <= F . g by YELLOW_0:60; ::_thesis: verum end; begin definition let S be non empty RelStr ; let T be non empty reflexive antisymmetric RelStr ; func UPS (S,T) -> strict RelStr means :Def4: :: WAYBEL27:def 4 ( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of it iff x is directed-sups-preserving Function of S,T ) ) ); 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 x is directed-sups-preserving Function of S,T ) ) ) proof defpred S1[ set ] means \$1 is directed-sups-preserving Function of S,T; 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 x is directed-sups-preserving Function of S,T ) ) ) thus SX is full SubRelStr of T |^ the carrier of S ; ::_thesis: for x being set holds ( x in the carrier of SX iff x is directed-sups-preserving Function of S,T ) let f be set ; ::_thesis: ( f in the carrier of SX iff f is directed-sups-preserving Function of S,T ) thus ( f in the carrier of SX implies f is directed-sups-preserving Function of S,T ) ::_thesis: ( f is directed-sups-preserving Function of S,T implies f in the carrier of SX ) proof assume f in the carrier of SX ; ::_thesis: f is directed-sups-preserving Function of S,T then f in X by YELLOW_0:def_15; hence f is directed-sups-preserving Function of S,T by A1; ::_thesis: verum end; assume A2: f is directed-sups-preserving Function of S,T ; ::_thesis: f in the carrier of SX then f is Element of (T |^ the carrier of S) by WAYBEL24:19; then f in X by A1, A2; 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 x is directed-sups-preserving Function of S,T ) ) & b2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of b2 iff x is directed-sups-preserving Function of S,T ) ) holds b1 = b2 proof let U1, U2 be strict RelStr ; ::_thesis: ( U1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of U1 iff x is directed-sups-preserving Function of S,T ) ) & U2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds ( x in the carrier of U2 iff x is directed-sups-preserving Function of S,T ) ) implies U1 = U2 ) assume that A3: U1 is full SubRelStr of T |^ the carrier of S and A4: for x being set holds ( x in the carrier of U1 iff x is directed-sups-preserving Function of S,T ) and A5: U2 is full SubRelStr of T |^ the carrier of S and A6: for x being set holds ( x in the carrier of U2 iff x is directed-sups-preserving Function of S,T ) ; ::_thesis: U1 = U2 the carrier of U1 = the carrier of U2 proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of U2 c= the carrier of U1 let x be set ; ::_thesis: ( x in the carrier of U1 implies x in the carrier of U2 ) assume x in the carrier of U1 ; ::_thesis: x in the carrier of U2 then x is directed-sups-preserving Function of S,T by A4; hence x in the carrier of U2 by A6; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of U2 or x in the carrier of U1 ) assume x in the carrier of U2 ; ::_thesis: x in the carrier of U1 then x is directed-sups-preserving Function of S,T by A6; hence x in the carrier of U1 by A4; ::_thesis: verum end; hence U1 = U2 by A3, A5, YELLOW_0:57; ::_thesis: verum end; end; :: deftheorem Def4 defines UPS WAYBEL27:def_4_:_ for S being non empty RelStr for T being non empty reflexive antisymmetric RelStr for b3 being strict RelStr holds ( b3 = UPS (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 x is directed-sups-preserving Function of S,T ) ) ) ); registration let S be non empty RelStr ; let T be non empty reflexive antisymmetric RelStr ; cluster UPS (S,T) -> non empty constituted-Functions strict reflexive antisymmetric ; coherence ( not UPS (S,T) is empty & UPS (S,T) is reflexive & UPS (S,T) is antisymmetric & UPS (S,T) is constituted-Functions ) proof set f = the directed-sups-preserving Function of S,T; the directed-sups-preserving Function of S,T in the carrier of (UPS (S,T)) by Def4; then UPS (S,T) is non empty full SubRelStr of T |^ the carrier of S by Def4; hence ( not UPS (S,T) is empty & UPS (S,T) is reflexive & UPS (S,T) is antisymmetric & UPS (S,T) is constituted-Functions ) ; ::_thesis: verum end; end; registration let S be non empty RelStr ; let T be non empty Poset; cluster UPS (S,T) -> strict transitive ; coherence UPS (S,T) is transitive proof UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; hence UPS (S,T) is transitive ; ::_thesis: verum end; end; theorem Th22: :: WAYBEL27:22 for S being non empty RelStr for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T) proof let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T) let T be non empty reflexive antisymmetric RelStr ; ::_thesis: the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T) UPS (S,T) is SubRelStr of T |^ the carrier of S by Def4; then the carrier of (UPS (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13; hence the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28; ::_thesis: verum end; definition let S be non empty RelStr ; let T be non empty reflexive antisymmetric RelStr ; let f be Element of (UPS (S,T)); let s be Element of S; :: original: . redefine funcf . s -> Element of T; coherence f . s is Element of T proof UPS (S,T) is SubRelStr of T |^ the carrier of S by Def4; then reconsider p = f as Element of (T |^ the carrier of S) by YELLOW_0:58; p . s = p . s ; hence f . s is Element of T ; ::_thesis: verum end; end; theorem Th23: :: WAYBEL27:23 for S being non empty RelStr for T being non empty reflexive antisymmetric RelStr for f, g being Element of (UPS (S,T)) holds ( f <= g iff for s being Element of S holds f . s <= g . s ) proof let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric RelStr for f, g being Element of (UPS (S,T)) holds ( f <= g iff for s being Element of S holds f . s <= g . s ) let T be non empty reflexive antisymmetric RelStr ; ::_thesis: for f, g being Element of (UPS (S,T)) holds ( f <= g iff for s being Element of S holds f . s <= g . s ) let f, g be Element of (UPS (S,T)); ::_thesis: ( f <= g iff for s being Element of S holds f . s <= g . s ) A1: UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; then reconsider a = f, b = g as Element of (T |^ the carrier of S) by YELLOW_0:58; A2: ( f <= g iff a <= b ) by A1, YELLOW_0:59, YELLOW_0:60; hence ( f <= g implies for s being Element of S holds f . s <= g . s ) by Th14; ::_thesis: ( ( for s being Element of S holds f . s <= g . s ) implies f <= g ) assume for s being Element of S holds f . s <= g . s ; ::_thesis: f <= g hence f <= g by A2, Th14; ::_thesis: verum end; theorem Th24: :: WAYBEL27:24 for S, T being complete Scott TopLattice holds UPS (S,T) = SCMaps (S,T) proof let S, T be complete Scott TopLattice; ::_thesis: UPS (S,T) = SCMaps (S,T) A1: the carrier of (UPS (S,T)) = the carrier of (SCMaps (S,T)) proof thus the carrier of (UPS (S,T)) c= the carrier of (SCMaps (S,T)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (SCMaps (S,T)) c= the carrier of (UPS (S,T)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (UPS (S,T)) or x in the carrier of (SCMaps (S,T)) ) assume x in the carrier of (UPS (S,T)) ; ::_thesis: x in the carrier of (SCMaps (S,T)) then reconsider f = x as directed-sups-preserving Function of S,T by Def4; f is continuous ; hence x in the carrier of (SCMaps (S,T)) by WAYBEL17:def_2; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (SCMaps (S,T)) or x in the carrier of (UPS (S,T)) ) assume A2: x in the carrier of (SCMaps (S,T)) ; ::_thesis: x in the carrier of (UPS (S,T)) the carrier of (SCMaps (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13; then reconsider f = x as Function of S,T by A2, WAYBEL10:9; f is continuous by A2, WAYBEL17:def_2; hence x in the carrier of (UPS (S,T)) by Def4; ::_thesis: verum end; then A3: the carrier of (UPS (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13; UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; then the InternalRel of (UPS (S,T)) = the InternalRel of (T |^ the carrier of S) |_2 the carrier of (UPS (S,T)) by YELLOW_0:def_14 .= ( the InternalRel of (T |^ the carrier of S) |_2 the carrier of (MonMaps (S,T))) |_2 the carrier of (UPS (S,T)) by A3, WELLORD1:22 .= the InternalRel of (MonMaps (S,T)) |_2 the carrier of (SCMaps (S,T)) by A1, YELLOW_0:def_14 .= the InternalRel of (SCMaps (S,T)) by YELLOW_0:def_14 ; hence UPS (S,T) = SCMaps (S,T) by A1; ::_thesis: verum end; theorem Th25: :: WAYBEL27:25 for S, S9 being non empty RelStr for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds UPS (S,T) = UPS (S9,T9) proof let S, S9 be non empty RelStr ; ::_thesis: for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds UPS (S,T) = UPS (S9,T9) let T, T9 be non empty reflexive antisymmetric RelStr ; ::_thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) implies UPS (S,T) = UPS (S9,T9) ) assume that A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) and A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) ; ::_thesis: UPS (S,T) = UPS (S9,T9) T |^ the carrier of S = T9 |^ the carrier of S9 by A1, A2, Th15; then A3: UPS (S9,T9) is full SubRelStr of T |^ the carrier of S by Def4; A4: the carrier of (UPS (S,T)) = the carrier of (UPS (S9,T9)) proof thus the carrier of (UPS (S,T)) c= the carrier of (UPS (S9,T9)) :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (UPS (S9,T9)) c= the carrier of (UPS (S,T)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (UPS (S,T)) or x in the carrier of (UPS (S9,T9)) ) assume x in the carrier of (UPS (S,T)) ; ::_thesis: x in the carrier of (UPS (S9,T9)) then reconsider x1 = x as directed-sups-preserving Function of S,T by Def4; reconsider y = x1 as Function of S9,T9 by A1, A2; y is directed-sups-preserving proof let X be Subset of S9; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or y preserves_sup_of X ) reconsider Y = X as Subset of S by A1; assume ( not X is empty & X is directed ) ; ::_thesis: y preserves_sup_of X then ( not Y is empty & Y is directed ) by A1, WAYBEL_0:3; then x1 preserves_sup_of Y by WAYBEL_0:def_37; hence y preserves_sup_of X by A1, A2, WAYBEL_0:65; ::_thesis: verum end; hence x in the carrier of (UPS (S9,T9)) by Def4; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (UPS (S9,T9)) or x in the carrier of (UPS (S,T)) ) assume x in the carrier of (UPS (S9,T9)) ; ::_thesis: x in the carrier of (UPS (S,T)) then reconsider x1 = x as directed-sups-preserving Function of S9,T9 by Def4; reconsider y = x1 as Function of S,T by A1, A2; y is directed-sups-preserving proof let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or y preserves_sup_of X ) reconsider Y = X as Subset of S9 by A1; assume ( not X is empty & X is directed ) ; ::_thesis: y preserves_sup_of X then ( not Y is empty & Y is directed ) by A1, WAYBEL_0:3; then x1 preserves_sup_of Y by WAYBEL_0:def_37; hence y preserves_sup_of X by A1, A2, WAYBEL_0:65; ::_thesis: verum end; hence x in the carrier of (UPS (S,T)) by Def4; ::_thesis: verum end; UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; hence UPS (S,T) = UPS (S9,T9) by A3, A4, YELLOW_0:57; ::_thesis: verum end; registration let S, T be complete LATTICE; cluster UPS (S,T) -> strict complete ; coherence UPS (S,T) is complete proof set T9 = the Scott TopAugmentation of T; set S9 = the Scott TopAugmentation of S; reconsider S9 = the Scott TopAugmentation of S, T9 = the Scott TopAugmentation of T as complete Scott TopLattice ; A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) by YELLOW_9:def_4; RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) by YELLOW_9:def_4; then UPS (S,T) = UPS (S9,T9) by A1, Th25 .= SCMaps (S9,T9) by Th24 .= ContMaps (S9,T9) by WAYBEL24:38 ; hence UPS (S,T) is complete ; ::_thesis: verum end; end; theorem Th26: :: WAYBEL27:26 for S, T being complete LATTICE holds UPS (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S proof let S, T be complete LATTICE; ::_thesis: UPS (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S set S9 = the Scott TopAugmentation of S; set T9 = the Scott TopAugmentation of T; A1: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) by YELLOW_9:def_4; then A2: the Scott TopAugmentation of T |^ the carrier of S = T |^ the carrier of S by Th15; A3: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) by YELLOW_9:def_4; then UPS (S,T) = UPS ( the Scott TopAugmentation of S, the Scott TopAugmentation of T) by A1, Th25 .= SCMaps ( the Scott TopAugmentation of S, the Scott TopAugmentation of T) by Th24 .= ContMaps ( the Scott TopAugmentation of S, the Scott TopAugmentation of T) by WAYBEL24:38 ; hence UPS (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S by A2, A3, WAYBEL24:35; ::_thesis: verum end; theorem Th27: :: WAYBEL27:27 for S, T being complete LATTICE for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S)) proof let S, T be complete LATTICE; ::_thesis: for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S)) let A be Subset of (UPS (S,T)); ::_thesis: sup A = "\/" (A,(T |^ the carrier of S)) A1: UPS (S,T) is full sups-inheriting SubRelStr of T |^ the carrier of S by Def4, Th26; ex_sup_of A,T |^ the carrier of S by YELLOW_0:17; then "\/" (A,(T |^ the carrier of S)) in the carrier of (UPS (S,T)) by A1, YELLOW_0:def_19; hence sup A = "\/" (A,(T |^ the carrier of S)) by A1, YELLOW_0:68; ::_thesis: verum end; definition let S1, S2, T1, T2 be non empty reflexive antisymmetric RelStr ; let f be Function of S1,S2; assume B1: f is directed-sups-preserving ; let g be Function of T1,T2; assume A2: g is directed-sups-preserving ; func UPS (f,g) -> Function of (UPS (S2,T1)),(UPS (S1,T2)) means :Def5: :: WAYBEL27:def 5 for h being directed-sups-preserving Function of S2,T1 holds it . h = (g * h) * f; existence ex b1 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f proof defpred S1[ set , set ] means for h being Function st h = \$1 holds \$2 = (g * h) * f; A1: for x being Element of (UPS (S2,T1)) ex y being Element of (UPS (S1,T2)) st S1[x,y] proof let x be Element of (UPS (S2,T1)); ::_thesis: ex y being Element of (UPS (S1,T2)) st S1[x,y] reconsider h = x as directed-sups-preserving Function of S2,T1 by Def4; h * f is directed-sups-preserving Function of S1,T1 by B1, WAYBEL20:28; then g * (h * f) is directed-sups-preserving Function of S1,T2 by A2, WAYBEL20:28; then (g * h) * f is directed-sups-preserving Function of S1,T2 by RELAT_1:36; then reconsider y = (g * h) * f as Element of (UPS (S1,T2)) by Def4; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider j being Function of the carrier of (UPS (S2,T1)), the carrier of (UPS (S1,T2)) such that A2: for x being Element of (UPS (S2,T1)) holds S1[x,j . x] from FUNCT_2:sch_3(A1); reconsider F = j as Function of (UPS (S2,T1)),(UPS (S1,T2)) ; take F ; ::_thesis: for h being directed-sups-preserving Function of S2,T1 holds F . h = (g * h) * f let h be directed-sups-preserving Function of S2,T1; ::_thesis: F . h = (g * h) * f h is Element of (UPS (S2,T1)) by Def4; hence F . h = (g * h) * f by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of (UPS (S2,T1)),(UPS (S1,T2)) st ( for h being directed-sups-preserving Function of S2,T1 holds b1 . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds b2 . h = (g * h) * f ) holds b1 = b2 proof let U1, U2 be Function of (UPS (S2,T1)),(UPS (S1,T2)); ::_thesis: ( ( for h being directed-sups-preserving Function of S2,T1 holds U1 . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds U2 . h = (g * h) * f ) implies U1 = U2 ) assume that A3: for h being directed-sups-preserving Function of S2,T1 holds U1 . h = (g * h) * f and A4: for h being directed-sups-preserving Function of S2,T1 holds U2 . h = (g * h) * f ; ::_thesis: U1 = U2 for x being set st x in the carrier of (UPS (S2,T1)) holds U1 . x = U2 . x proof let x be set ; ::_thesis: ( x in the carrier of (UPS (S2,T1)) implies U1 . x = U2 . x ) assume x in the carrier of (UPS (S2,T1)) ; ::_thesis: U1 . x = U2 . x then reconsider h = x as directed-sups-preserving Function of S2,T1 by Def4; thus U1 . x = (g * h) * f by A3 .= U2 . x by A4 ; ::_thesis: verum end; hence U1 = U2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def5 defines UPS WAYBEL27:def_5_:_ for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr for f being Function of S1,S2 st f is directed-sups-preserving holds for g being Function of T1,T2 st g is directed-sups-preserving holds for b7 being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds ( b7 = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b7 . h = (g * h) * f ); theorem Th28: :: WAYBEL27:28 for S1, S2, S3, T1, T2, T3 being non empty Poset for f1 being directed-sups-preserving Function of S2,S3 for f2 being directed-sups-preserving Function of S1,S2 for g1 being directed-sups-preserving Function of T1,T2 for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) proof let S1, S2, S3, T1, T2, T3 be non empty Poset; ::_thesis: for f1 being directed-sups-preserving Function of S2,S3 for f2 being directed-sups-preserving Function of S1,S2 for g1 being directed-sups-preserving Function of T1,T2 for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) let f1 be directed-sups-preserving Function of S2,S3; ::_thesis: for f2 being directed-sups-preserving Function of S1,S2 for g1 being directed-sups-preserving Function of T1,T2 for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) let f2 be directed-sups-preserving Function of S1,S2; ::_thesis: for g1 being directed-sups-preserving Function of T1,T2 for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) let g1 be directed-sups-preserving Function of T1,T2; ::_thesis: for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) let g2 be directed-sups-preserving Function of T2,T3; ::_thesis: (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) reconsider F = f1 * f2 as directed-sups-preserving Function of S1,S3 by WAYBEL20:28; reconsider G = g2 * g1 as directed-sups-preserving Function of T1,T3 by WAYBEL20:28; for h being directed-sups-preserving Function of S3,T1 holds ((UPS (f2,g2)) * (UPS (f1,g1))) . h = (G * h) * F proof let h be directed-sups-preserving Function of S3,T1; ::_thesis: ((UPS (f2,g2)) * (UPS (f1,g1))) . h = (G * h) * F g1 * h is directed-sups-preserving Function of S3,T2 by WAYBEL20:28; then reconsider ghf = (g1 * h) * f1 as directed-sups-preserving Function of S2,T2 by WAYBEL20:28; dom (UPS (f1,g1)) = the carrier of (UPS (S3,T1)) by FUNCT_2:def_1; then h in dom (UPS (f1,g1)) by Def4; then ((UPS (f2,g2)) * (UPS (f1,g1))) . h = (UPS (f2,g2)) . ((UPS (f1,g1)) . h) by FUNCT_1:13 .= (UPS (f2,g2)) . ((g1 * h) * f1) by Def5 ; hence ((UPS (f2,g2)) * (UPS (f1,g1))) . h = (g2 * ghf) * f2 by Def5 .= g2 * (((g1 * h) * f1) * f2) by RELAT_1:36 .= g2 * ((g1 * (h * f1)) * f2) by RELAT_1:36 .= g2 * (g1 * ((h * f1) * f2)) by RELAT_1:36 .= g2 * (g1 * (h * (f1 * f2))) by RELAT_1:36 .= g2 * ((g1 * h) * (f1 * f2)) by RELAT_1:36 .= (g2 * (g1 * h)) * (f1 * f2) by RELAT_1:36 .= (G * h) * F by RELAT_1:36 ; ::_thesis: verum end; hence (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1)) by Def5; ::_thesis: verum end; theorem Th29: :: WAYBEL27:29 for S, T being non empty reflexive antisymmetric RelStr holds UPS ((id S),(id T)) = id (UPS (S,T)) proof let S, T be non empty reflexive antisymmetric RelStr ; ::_thesis: UPS ((id S),(id T)) = id (UPS (S,T)) A1: for x being set st x in the carrier of (UPS (S,T)) holds (UPS ((id S),(id T))) . x = x proof let x be set ; ::_thesis: ( x in the carrier of (UPS (S,T)) implies (UPS ((id S),(id T))) . x = x ) assume x in the carrier of (UPS (S,T)) ; ::_thesis: (UPS ((id S),(id T))) . x = x then reconsider f = x as directed-sups-preserving Function of S,T by Def4; (UPS ((id S),(id T))) . f = ((id T) * f) * (id S) by Def5 .= f * (id S) by FUNCT_2:17 ; hence (UPS ((id S),(id T))) . x = x by FUNCT_2:17; ::_thesis: verum end; dom (UPS ((id S),(id T))) = the carrier of (UPS (S,T)) by FUNCT_2:def_1; hence UPS ((id S),(id T)) = id (UPS (S,T)) by A1, FUNCT_1:17; ::_thesis: verum end; theorem Th30: :: WAYBEL27:30 for S1, S2, T1, T2 being complete LATTICE for f being directed-sups-preserving Function of S1,S2 for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving proof let S1, S2, T1, T2 be complete LATTICE; ::_thesis: for f being directed-sups-preserving Function of S1,S2 for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving let f be directed-sups-preserving Function of S1,S2; ::_thesis: for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving let g be directed-sups-preserving Function of T1,T2; ::_thesis: UPS (f,g) is directed-sups-preserving let A be Subset of (UPS (S2,T1)); :: according to WAYBEL_0:def_37 ::_thesis: ( A is empty or not A is directed or UPS (f,g) preserves_sup_of A ) assume ( not A is empty & A is directed ) ; ::_thesis: UPS (f,g) preserves_sup_of A then reconsider H = A as non empty directed Subset of (UPS (S2,T1)) ; assume ex_sup_of A, UPS (S2,T1) ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (UPS (f,g)) .: A, UPS (S1,T2) & "\/" (((UPS (f,g)) .: A),(UPS (S1,T2))) = (UPS (f,g)) . ("\/" (A,(UPS (S2,T1)))) ) thus ex_sup_of (UPS (f,g)) .: A, UPS (S1,T2) by YELLOW_0:17; ::_thesis: "\/" (((UPS (f,g)) .: A),(UPS (S1,T2))) = (UPS (f,g)) . ("\/" (A,(UPS (S2,T1)))) UPS (S2,T1) is full SubRelStr of T1 |^ the carrier of S2 by Def4; then reconsider B = H as non empty directed Subset of (T1 |^ the carrier of S2) by YELLOW_2:7; A1: UPS (S1,T2) is full SubRelStr of T2 |^ the carrier of S1 by Def4; then reconsider fgsA = (UPS (f,g)) . (sup H) as Element of (T2 |^ the carrier of S1) by YELLOW_0:58; the carrier of (UPS (S1,T2)) c= the carrier of (T2 |^ the carrier of S1) by A1, YELLOW_0:def_13; then reconsider fgA = (UPS (f,g)) .: H as non empty Subset of (T2 |^ the carrier of S1) by XBOOLE_1:1; A2: T2 |^ the carrier of S1 = product ( the carrier of S1 --> T2) by YELLOW_1:def_5; then A3: dom (sup fgA) = the carrier of S1 by WAYBEL_3:27; A4: T1 |^ the carrier of S2 = product ( the carrier of S2 --> T1) by YELLOW_1:def_5; A5: now__::_thesis:_for_s_being_set_st_s_in_the_carrier_of_S1_holds_ (sup_fgA)_._s_=_fgsA_._s reconsider BB = B as directed Subset of (product ( the carrier of S2 --> T1)) by A4; let s be set ; ::_thesis: ( s in the carrier of S1 implies (sup fgA) . s = fgsA . s ) A6: dom f = the carrier of S1 by FUNCT_2:def_1; assume s in the carrier of S1 ; ::_thesis: (sup fgA) . s = fgsA . s then reconsider x = s as Element of S1 ; reconsider sH = sup H as directed-sups-preserving Function of S2,T1 by Def4; A7: ( the carrier of S2 --> T1) . (f . x) = T1 by FUNCOP_1:7; dom sH = the carrier of S2 by FUNCT_2:def_1; then f . x in dom sH ; then A8: x in dom (sH * f) by A6, FUNCT_1:11; A9: pi (fgA,x) = g .: (pi (A,(f . x))) proof thus pi (fgA,x) c= g .: (pi (A,(f . x))) :: according to XBOOLE_0:def_10 ::_thesis: g .: (pi (A,(f . x))) c= pi (fgA,x) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (fgA,x) or a in g .: (pi (A,(f . x))) ) A10: dom g = the carrier of T1 by FUNCT_2:def_1; assume a in pi (fgA,x) ; ::_thesis: a in g .: (pi (A,(f . x))) then consider F being Function such that A11: F in fgA and A12: a = F . x by CARD_3:def_6; consider G being set such that A13: G in dom (UPS (f,g)) and A14: G in H and A15: F = (UPS (f,g)) . G by A11, FUNCT_1:def_6; reconsider G = G as directed-sups-preserving Function of S2,T1 by A13, Def4; A16: G . (f . x) in pi (A,(f . x)) by A14, CARD_3:def_6; A17: dom f = the carrier of S1 by FUNCT_2:def_1; dom G = the carrier of S2 by FUNCT_2:def_1; then f . x in dom G ; then A18: x in dom (G * f) by A17, FUNCT_1:11; a = ((g * G) * f) . x by A12, A15, Def5 .= (g * (G * f)) . x by RELAT_1:36 .= g . ((G * f) . x) by A18, FUNCT_1:13 .= g . (G . (f . x)) by A17, FUNCT_1:13 ; hence a in g .: (pi (A,(f . x))) by A10, A16, FUNCT_1:def_6; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in g .: (pi (A,(f . x))) or a in pi (fgA,x) ) A19: dom (UPS (f,g)) = the carrier of (UPS (S2,T1)) by FUNCT_2:def_1; assume a in g .: (pi (A,(f . x))) ; ::_thesis: a in pi (fgA,x) then consider F being set such that F in dom g and A20: F in pi (A,(f . x)) and A21: a = g . F by FUNCT_1:def_6; consider G being Function such that A22: G in A and A23: F = G . (f . x) by A20, CARD_3:def_6; reconsider G = G as directed-sups-preserving Function of S2,T1 by A22, Def4; (g * G) * f = (UPS (f,g)) . G by Def5; then A24: (g * G) * f in fgA by A22, A19, FUNCT_1:def_6; A25: dom f = the carrier of S1 by FUNCT_2:def_1; dom G = the carrier of S2 by FUNCT_2:def_1; then f . x in dom G ; then A26: x in dom (G * f) by A25, FUNCT_1:11; a = g . ((G * f) . x) by A21, A23, A25, FUNCT_1:13 .= (g * (G * f)) . x by A26, FUNCT_1:13 .= ((g * G) * f) . x by RELAT_1:36 ; hence a in pi (fgA,x) by A24, CARD_3:def_6; ::_thesis: verum end; A27: ex_sup_of pi (B,(f . x)),T1 by YELLOW_0:17; A28: pi (BB,(f . x)) is directed by YELLOW16:35; ( the carrier of S2 --> T1) . (f . x) = T1 by FUNCOP_1:7; then A29: g preserves_sup_of pi (B,(f . x)) by A28, WAYBEL_0:def_37; ( the carrier of S1 --> T2) . x = T2 by FUNCOP_1:7; hence (sup fgA) . s = sup (pi (fgA,x)) by A2, YELLOW16:33, YELLOW_0:17 .= g . (sup (pi (B,(f . x)))) by A9, A29, A27, WAYBEL_0:def_31 .= g . ((sup B) . (f . x)) by A4, A7, YELLOW16:33, YELLOW_0:17 .= g . (sH . (f . x)) by Th27 .= g . ((sH * f) . x) by A6, FUNCT_1:13 .= (g * (sH * f)) . x by A8, FUNCT_1:13 .= ((g * sH) * f) . s by RELAT_1:36 .= fgsA . s by Def5 ; ::_thesis: verum end; A30: dom fgsA = the carrier of S1 by A2, WAYBEL_3:27; thus sup ((UPS (f,g)) .: A) = sup fgA by Th27 .= (UPS (f,g)) . (sup A) by A3, A30, A5, FUNCT_1:2 ; ::_thesis: verum end; theorem Th31: :: WAYBEL27:31 Omega Sierpinski_Space is Scott proof BoolePoset 1 = InclPoset (bool 1) by YELLOW_1:4; then A1: the carrier of (BoolePoset 1) = {0,1} by YELLOW14:1, YELLOW_1:1; set S = the strict Scott TopAugmentation of BoolePoset 1; A2: the topology of the strict Scott TopAugmentation of BoolePoset 1 = the topology of Sierpinski_Space by WAYBEL18:12; A3: RelStr(# the carrier of the strict Scott TopAugmentation of BoolePoset 1, the InternalRel of the strict Scott TopAugmentation of BoolePoset 1 #) = BoolePoset 1 by YELLOW_9:def_4; the carrier of Sierpinski_Space = {0,1} by WAYBEL18:def_9; then Omega Sierpinski_Space = Omega the strict Scott TopAugmentation of BoolePoset 1 by A2, A3, A1, WAYBEL25:13 .= the strict Scott TopAugmentation of BoolePoset 1 by WAYBEL25:15 ; hence Omega Sierpinski_Space is Scott ; ::_thesis: verum end; theorem :: WAYBEL27:32 for S being complete Scott TopLattice holds oContMaps (S,Sierpinski_Space) = UPS (S,(BoolePoset 1)) proof reconsider B1 = BoolePoset 1 as complete LATTICE ; reconsider OSS = Omega Sierpinski_Space as complete Scott TopAugmentation of B1 by Th31, WAYBEL26:4; let S be complete Scott TopLattice; ::_thesis: oContMaps (S,Sierpinski_Space) = UPS (S,(BoolePoset 1)) A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S, the InternalRel of S #) ; TopStruct(# the carrier of OSS, the topology of OSS #) = TopStruct(# the carrier of Sierpinski_Space, the topology of Sierpinski_Space #) by WAYBEL25:def_2; then Omega OSS = OSS by WAYBEL25:13; then A2: RelStr(# the carrier of OSS, the InternalRel of OSS #) = RelStr(# the carrier of B1, the InternalRel of B1 #) by WAYBEL25:16; thus oContMaps (S,Sierpinski_Space) = ContMaps (S,(Omega Sierpinski_Space)) by WAYBEL26:def_1 .= SCMaps (S,OSS) by WAYBEL24:38 .= UPS (S,OSS) by Th24 .= UPS (S,(BoolePoset 1)) by A1, A2, Th25 ; ::_thesis: verum end; theorem Th33: :: WAYBEL27:33 for S being complete LATTICE ex F being Function of (UPS (S,(BoolePoset 1))),(InclPoset (sigma S)) st ( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) ) proof set T = BoolePoset 1; reconsider T9 = Omega Sierpinski_Space as Scott TopAugmentation of BoolePoset 1 by Th31, WAYBEL26:4; let S be complete LATTICE; ::_thesis: ex F being Function of (UPS (S,(BoolePoset 1))),(InclPoset (sigma S)) st ( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) ) set S9 = the Scott TopAugmentation of S; A1: BoolePoset 1 = RelStr(# the carrier of T9, the InternalRel of T9 #) by YELLOW_9:def_4; A2: the topology of the Scott TopAugmentation of S = sigma S by YELLOW_9:51; RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) by YELLOW_9:def_4; then UPS (S,(BoolePoset 1)) = UPS ( the Scott TopAugmentation of S,T9) by A1, Th25 .= SCMaps ( the Scott TopAugmentation of S,T9) by Th24 .= ContMaps ( the Scott TopAugmentation of S,T9) by WAYBEL24:38 .= oContMaps ( the Scott TopAugmentation of S,Sierpinski_Space) by WAYBEL26:def_1 ; then consider G being Function of (InclPoset (sigma S)),(UPS (S,(BoolePoset 1))) such that A3: G is isomorphic and A4: for V being open Subset of the Scott TopAugmentation of S holds G . V = chi (V, the carrier of the Scott TopAugmentation of S) by A2, WAYBEL26:5; take F = G " ; ::_thesis: ( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} ) ) A5: rng G = [#] (UPS (S,(BoolePoset 1))) by A3, WAYBEL_0:66; then G is onto by FUNCT_2:def_3; then A6: F = G " by A3, TOPS_2:def_4; hence F is isomorphic by A3, WAYBEL_0:68; ::_thesis: for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} let f be directed-sups-preserving Function of S,(BoolePoset 1); ::_thesis: F . f = f " {1} f in the carrier of (UPS (S,(BoolePoset 1))) by Def4; then consider V being set such that A7: V in dom G and A8: f = G . V by A5, FUNCT_1:def_3; dom G = the carrier of (InclPoset (sigma S)) by FUNCT_2:def_1 .= sigma S by YELLOW_1:1 ; then reconsider V = V as open Subset of the Scott TopAugmentation of S by A2, A7, PRE_TOPC:def_2; thus F . f = V by A3, A6, A7, A8, FUNCT_1:34 .= (chi (V, the carrier of the Scott TopAugmentation of S)) " {1} by Th13 .= f " {1} by A4, A8 ; ::_thesis: verum end; theorem Th34: :: WAYBEL27:34 for S being complete LATTICE holds UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic proof let S be complete LATTICE; ::_thesis: UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic consider F being Function of (UPS (S,(BoolePoset 1))),(InclPoset (sigma S)) such that A1: F is isomorphic and for f being directed-sups-preserving Function of S,(BoolePoset 1) holds F . f = f " {1} by Th33; take F ; :: according to WAYBEL_1:def_8 ::_thesis: F is isomorphic thus F is isomorphic by A1; ::_thesis: verum end; theorem Th35: :: WAYBEL27:35 for S1, S2, T1, T2 being complete LATTICE for f being Function of S1,S2 for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds UPS (f,g) is isomorphic proof let S1, S2, T1, T2 be complete LATTICE; ::_thesis: for f being Function of S1,S2 for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds UPS (f,g) is isomorphic let f be Function of S1,S2; ::_thesis: for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds UPS (f,g) is isomorphic let g be Function of T1,T2; ::_thesis: ( f is isomorphic & g is isomorphic implies UPS (f,g) is isomorphic ) assume that A1: f is isomorphic and A2: g is isomorphic ; ::_thesis: UPS (f,g) is isomorphic A3: g is sups-preserving Function of T1,T2 by A2, WAYBEL13:20; A4: f is sups-preserving Function of S1,S2 by A1, WAYBEL13:20; then A5: UPS (f,g) is directed-sups-preserving Function of (UPS (S2,T1)),(UPS (S1,T2)) by A3, Th30; consider g9 being monotone Function of T2,T1 such that A6: g * g9 = id T2 and A7: g9 * g = id T1 by A2, YELLOW16:15; g9 is isomorphic by A2, A6, A7, YELLOW16:15; then A8: g9 is sups-preserving Function of T2,T1 by WAYBEL13:20; consider f9 being monotone Function of S2,S1 such that A9: f * f9 = id S2 and A10: f9 * f = id S1 by A1, YELLOW16:15; f9 is isomorphic by A1, A9, A10, YELLOW16:15; then A11: f9 is sups-preserving Function of S2,S1 by WAYBEL13:20; then A12: UPS (f9,g9) is directed-sups-preserving Function of (UPS (S1,T2)),(UPS (S2,T1)) by A8, Th30; A13: (UPS (f9,g9)) * (UPS (f,g)) = UPS ((id S2),(id T1)) by A4, A3, A9, A7, A11, A8, Th28 .= id (UPS (S2,T1)) by Th29 ; (UPS (f,g)) * (UPS (f9,g9)) = UPS ((id S1),(id T2)) by A4, A3, A10, A6, A11, A8, Th28 .= id (UPS (S1,T2)) by Th29 ; hence UPS (f,g) is isomorphic by A13, A5, A12, YELLOW16:15; ::_thesis: verum end; theorem Th36: :: WAYBEL27:36 for S1, S2, T1, T2 being complete LATTICE st S1,S2 are_isomorphic & T1,T2 are_isomorphic holds UPS (S2,T1), UPS (S1,T2) are_isomorphic proof let S1, S2, T1, T2 be complete LATTICE; ::_thesis: ( S1,S2 are_isomorphic & T1,T2 are_isomorphic implies UPS (S2,T1), UPS (S1,T2) are_isomorphic ) given f being Function of S1,S2 such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not T1,T2 are_isomorphic or UPS (S2,T1), UPS (S1,T2) are_isomorphic ) given g being Function of T1,T2 such that A2: g is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: UPS (S2,T1), UPS (S1,T2) are_isomorphic take UPS (f,g) ; :: according to WAYBEL_1:def_8 ::_thesis: UPS (f,g) is isomorphic thus UPS (f,g) is isomorphic by A1, A2, Th35; ::_thesis: verum end; theorem Th37: :: WAYBEL27:37 for S, T being complete LATTICE for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f)) proof let S, T be complete LATTICE; ::_thesis: for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f)) let f be directed-sups-preserving projection Function of T,T; ::_thesis: Image (UPS ((id S),f)) = UPS (S,(Image f)) reconsider If = Image f as complete LATTICE by YELLOW_2:35; A1: If |^ the carrier of S is full SubRelStr of T |^ the carrier of S by YELLOW16:39; UPS (S,If) is full SubRelStr of (Image f) |^ the carrier of S by Def4; then reconsider UPSIf = UPS (S,If) as full SubRelStr of T |^ the carrier of S by A1, WAYBEL15:1; UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; then reconsider IUPS = Image (UPS ((id S),f)) as full SubRelStr of T |^ the carrier of S by WAYBEL15:1; the carrier of UPSIf = the carrier of IUPS proof thus the carrier of UPSIf c= the carrier of IUPS :: according to XBOOLE_0:def_10 ::_thesis: the carrier of IUPS c= the carrier of UPSIf proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of UPSIf or x in the carrier of IUPS ) A2: dom (UPS ((id S),f)) = the carrier of (UPS (S,T)) by FUNCT_2:def_1; assume x in the carrier of UPSIf ; ::_thesis: x in the carrier of IUPS then reconsider h = x as directed-sups-preserving Function of S,If by Def4; the carrier of If c= the carrier of T by YELLOW_0:def_13; then A3: rng h c= the carrier of T by XBOOLE_1:1; dom h = the carrier of S by FUNCT_2:def_1; then reconsider g = h as Function of S,T by A3, RELSET_1:4; A4: g is directed-sups-preserving proof let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or g preserves_sup_of X ) assume A5: ( not X is empty & X is directed ) ; ::_thesis: g preserves_sup_of X thus g preserves_sup_of X ::_thesis: verum proof reconsider hX = h .: X as non empty directed Subset of If by A5, YELLOW_2:15; assume A6: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: X,T & "\/" ((g .: X),T) = g . ("\/" (X,S)) ) h preserves_sup_of X by A5, WAYBEL_0:def_37; then A7: sup hX = h . (sup X) by A6, WAYBEL_0:def_31; thus A8: ex_sup_of g .: X,T by YELLOW_0:17; ::_thesis: "\/" ((g .: X),T) = g . ("\/" (X,S)) If is non empty full directed-sups-inheriting SubRelStr of T by YELLOW_2:35; hence "\/" ((g .: X),T) = g . ("\/" (X,S)) by A7, A8, WAYBEL_0:7; ::_thesis: verum end; end; then A9: g in the carrier of (UPS (S,T)) by Def4; (UPS ((id S),f)) . g = (f * g) * (id S) by A4, Def5 .= h * (id S) by Th10 .= g by FUNCT_2:17 ; then x in rng (UPS ((id S),f)) by A9, A2, FUNCT_1:def_3; hence x in the carrier of IUPS by YELLOW_0:def_15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of IUPS or x in the carrier of UPSIf ) A10: rng f = the carrier of (subrelstr (rng f)) by YELLOW_0:def_15; assume x in the carrier of IUPS ; ::_thesis: x in the carrier of UPSIf then x in rng (UPS ((id S),f)) by YELLOW_0:def_15; then consider a being set such that A11: a in dom (UPS ((id S),f)) and A12: x = (UPS ((id S),f)) . a by FUNCT_1:def_3; reconsider a = a as directed-sups-preserving Function of S,T by A11, Def4; A13: x = (f * a) * (id S) by A12, Def5 .= f * a by FUNCT_2:17 ; then reconsider x0 = x as directed-sups-preserving Function of S,T by WAYBEL15:11; A14: rng x0 c= the carrier of T ; dom x0 = the carrier of S by FUNCT_2:def_1; then reconsider x1 = x0 as Function of S,If by A10, A13, A14, FUNCT_2:2, RELAT_1:26; x1 is directed-sups-preserving proof let X be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( X is empty or not X is directed or x1 preserves_sup_of X ) assume A15: ( not X is empty & X is directed ) ; ::_thesis: x1 preserves_sup_of X thus x1 preserves_sup_of X ::_thesis: verum proof reconsider hX = x0 .: X as non empty directed Subset of T by A15, YELLOW_2:15; A16: If is non empty full directed-sups-inheriting SubRelStr of T by YELLOW_2:35; reconsider gX = x1 .: X as non empty directed Subset of If by Th12, A15, YELLOW_2:15; assume A17: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of x1 .: X,If & "\/" ((x1 .: X),If) = x1 . ("\/" (X,S)) ) thus ex_sup_of x1 .: X,If by YELLOW_0:17; ::_thesis: "\/" ((x1 .: X),If) = x1 . ("\/" (X,S)) A18: x0 preserves_sup_of X by A15, WAYBEL_0:def_37; then ex_sup_of x0 .: X,T by A17, WAYBEL_0:def_31; then sup gX = sup hX by A16, WAYBEL_0:7; hence "\/" ((x1 .: X),If) = x1 . ("\/" (X,S)) by A17, A18, WAYBEL_0:def_31; ::_thesis: verum end; end; hence x in the carrier of UPSIf by Def4; ::_thesis: verum end; hence Image (UPS ((id S),f)) = UPS (S,(Image f)) by YELLOW_0:57; ::_thesis: verum end; Lm1: now__::_thesis:_for_M_being_non_empty_set_ for_X,_Y_being_non_empty_Poset for_f_being_directed-sups-preserving_Function_of_X,(Y_|^_M)_holds_ (_f_in_Funcs_(_the_carrier_of_X,(Funcs_(M,_the_carrier_of_Y)))_&_rng_(commute_f)_c=_Funcs_(_the_carrier_of_X,_the_carrier_of_Y)_&_dom_(commute_f)_=_M_) let M be non empty set ; ::_thesis: for X, Y being non empty Poset for f being directed-sups-preserving Function of X,(Y |^ M) holds ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) let X, Y be non empty Poset; ::_thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) let f be directed-sups-preserving Function of X,(Y |^ M); ::_thesis: ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) the carrier of (Y |^ M) = Funcs (M, the carrier of Y) by YELLOW_1:28; then A1: rng f c= Funcs (M, the carrier of Y) ; dom f = the carrier of X by FUNCT_2:def_1; hence f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by A1, FUNCT_2:def_2; ::_thesis: ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) then commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:55; then ex g being Function st ( commute f = g & dom g = M & rng g c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def_2; hence ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) ; ::_thesis: verum end; theorem Th38: :: WAYBEL27:38 for X being non empty set for S, T being non empty Poset for f being directed-sups-preserving Function of S,(T |^ X) for i being Element of X holds (commute f) . i is directed-sups-preserving Function of S,T proof let M be non empty set ; ::_thesis: for S, T being non empty Poset for f being directed-sups-preserving Function of S,(T |^ M) for i being Element of M holds (commute f) . i is directed-sups-preserving Function of S,T let X, Y be non empty Poset; ::_thesis: for f being directed-sups-preserving Function of X,(Y |^ M) for i being Element of M holds (commute f) . i is directed-sups-preserving Function of X,Y let f be directed-sups-preserving Function of X,(Y |^ M); ::_thesis: for i being Element of M holds (commute f) . i is directed-sups-preserving Function of X,Y let i be Element of M; ::_thesis: (commute f) . i is directed-sups-preserving Function of X,Y A1: (M --> Y) . i = Y by FUNCOP_1:7; dom (commute f) = M by Lm1; then A2: (commute f) . i in rng (commute f) by FUNCT_1:def_3; A3: f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by Lm1; then f is Function of the carrier of X,(Funcs (M, the carrier of Y)) by FUNCT_2:66; then A4: rng f c= Funcs (M, the carrier of Y) by RELAT_1:def_19; rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) by Lm1; then consider g being Function such that A5: (commute f) . i = g and A6: dom g = the carrier of X and A7: rng g c= the carrier of Y by A2, FUNCT_2:def_2; reconsider g = g as Function of X,Y by A6, A7, FUNCT_2:2; A8: Y |^ M = product (M --> Y) by YELLOW_1:def_5; g is directed-sups-preserving proof let A be Subset of X; :: according to WAYBEL_0:def_37 ::_thesis: ( A is empty or not A is directed or g preserves_sup_of A ) assume ( not A is empty & A is directed ) ; ::_thesis: g preserves_sup_of A then reconsider B = A as non empty directed Subset of X ; assume A9: ex_sup_of A,X ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: A,Y & "\/" ((g .: A),Y) = g . ("\/" (A,X)) ) A10: f preserves_sup_of B by WAYBEL_0:def_37; then A11: ex_sup_of f .: B,Y |^ M by A9, WAYBEL_0:def_31; then ex_sup_of pi ((f .: A),i),Y by A8, A1, YELLOW16:31; hence ex_sup_of g .: A,Y by A4, A5, Th8; ::_thesis: "\/" ((g .: A),Y) = g . ("\/" (A,X)) A12: pi ((f .: A),i) = g .: A by A4, A5, Th8; sup (f .: B) = f . (sup B) by A9, A10, WAYBEL_0:def_31; then sup (pi ((f .: A),i)) = (f . (sup A)) . i by A11, A8, A1, YELLOW16:33; hence "\/" ((g .: A),Y) = g . ("\/" (A,X)) by A3, A5, A12, FUNCT_6:56; ::_thesis: verum end; hence (commute f) . i is directed-sups-preserving Function of X,Y by A5; ::_thesis: verum end; theorem Th39: :: WAYBEL27:39 for X being non empty set for S, T being non empty Poset for f being directed-sups-preserving Function of S,(T |^ X) holds commute f is Function of X, the carrier of (UPS (S,T)) proof let M be non empty set ; ::_thesis: for S, T being non empty Poset for f being directed-sups-preserving Function of S,(T |^ M) holds commute f is Function of M, the carrier of (UPS (S,T)) let X, Y be non empty Poset; ::_thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds commute f is Function of M, the carrier of (UPS (X,Y)) let f be directed-sups-preserving Function of X,(Y |^ M); ::_thesis: commute f is Function of M, the carrier of (UPS (X,Y)) A1: rng (commute f) c= the carrier of (UPS (X,Y)) proof let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng (commute f) or g in the carrier of (UPS (X,Y)) ) assume g in rng (commute f) ; ::_thesis: g in the carrier of (UPS (X,Y)) then consider i being set such that A2: i in dom (commute f) and A3: g = (commute f) . i by FUNCT_1:def_3; reconsider i = i as Element of M by A2, Lm1; (commute f) . i is directed-sups-preserving Function of X,Y by Th38; hence g in the carrier of (UPS (X,Y)) by A3, Def4; ::_thesis: verum end; dom (commute f) = M by Lm1; hence commute f is Function of M, the carrier of (UPS (X,Y)) by A1, FUNCT_2:2; ::_thesis: verum end; theorem Th40: :: WAYBEL27:40 for X being non empty set for S, T being non empty Poset for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X) proof let X be non empty set ; ::_thesis: for S, T being non empty Poset for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X) let S, T be non empty Poset; ::_thesis: for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X) let f be Function of X, the carrier of (UPS (S,T)); ::_thesis: commute f is directed-sups-preserving Function of S,(T |^ X) A1: the carrier of (T |^ X) = Funcs (X, the carrier of T) by YELLOW_1:28; A2: f in Funcs (X, the carrier of (UPS (S,T))) by FUNCT_2:8; A3: Funcs (X, the carrier of (UPS (S,T))) c= Funcs (X,(Funcs ( the carrier of S, the carrier of T))) by Th22, FUNCT_5:56; then commute f in Funcs ( the carrier of S,(Funcs (X, the carrier of T))) by A2, FUNCT_6:55; then reconsider g = commute f as Function of S,(T |^ X) by A1, FUNCT_2:66; A4: rng g c= Funcs (X, the carrier of T) by A1; g is directed-sups-preserving proof let A be Subset of S; :: according to WAYBEL_0:def_37 ::_thesis: ( A is empty or not A is directed or g preserves_sup_of A ) assume ( not A is empty & A is directed ) ; ::_thesis: g preserves_sup_of A then reconsider B = A as non empty directed Subset of S ; A5: T |^ X = product (X --> T) by YELLOW_1:def_5; then A6: dom (g . (sup A)) = X by WAYBEL_3:27; assume A7: ex_sup_of A,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: A,T |^ X & "\/" ((g .: A),(T |^ X)) = g . ("\/" (A,S)) ) now__::_thesis:_for_x_being_Element_of_X_holds_ex_sup_of_pi_((g_.:_A),x),(X_-->_T)_._x let x be Element of X; ::_thesis: ex_sup_of pi ((g .: A),x),(X --> T) . x reconsider fx = f . x as directed-sups-preserving Function of S,T by Def4; A8: fx preserves_sup_of B by WAYBEL_0:def_37; commute g = f by A3, A2, FUNCT_6:57; then A9: fx .: A = pi ((g .: A),x) by A4, Th8; (X --> T) . x = T by FUNCOP_1:7; hence ex_sup_of pi ((g .: A),x),(X --> T) . x by A9, A8, A7, WAYBEL_0:def_31; ::_thesis: verum end; hence A10: ex_sup_of g .: A,T |^ X by A5, YELLOW16:31; ::_thesis: "\/" ((g .: A),(T |^ X)) = g . ("\/" (A,S)) A11: now__::_thesis:_for_x_being_set_st_x_in_X_holds_ (sup_(g_.:_A))_._x_=_(g_._(sup_A))_._x let x be set ; ::_thesis: ( x in X implies (sup (g .: A)) . x = (g . (sup A)) . x ) assume x in X ; ::_thesis: (sup (g .: A)) . x = (g . (sup A)) . x then reconsider a = x as Element of X ; reconsider fx = f . a as directed-sups-preserving Function of S,T by Def4; A12: (X --> T) . a = T by FUNCOP_1:7; commute g = f by A3, A2, FUNCT_6:57; then A13: fx .: A = pi ((g .: A),a) by A4, Th8; fx preserves_sup_of B by WAYBEL_0:def_37; then sup (pi ((g .: B),a)) = fx . (sup A) by A13, A7, WAYBEL_0:def_31; then fx . (sup A) = (sup (g .: B)) . a by A5, A10, A12, YELLOW16:33; hence (sup (g .: A)) . x = (g . (sup A)) . x by A3, A2, FUNCT_6:56; ::_thesis: verum end; dom (sup (g .: A)) = X by A5, WAYBEL_3:27; hence "\/" ((g .: A),(T |^ X)) = g . ("\/" (A,S)) by A11, A6, FUNCT_1:2; ::_thesis: verum end; hence commute f is directed-sups-preserving Function of S,(T |^ X) ; ::_thesis: verum end; theorem Th41: :: WAYBEL27:41 for X being non empty set for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st ( F is commuting & F is isomorphic ) proof deffunc H1( Function) -> set = commute \$1; let X be non empty set ; ::_thesis: for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st ( F is commuting & F is isomorphic ) let S, T be non empty Poset; ::_thesis: ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st ( F is commuting & F is isomorphic ) consider F being ManySortedSet of the carrier of (UPS (S,(T |^ X))) such that A1: for f being Element of (UPS (S,(T |^ X))) holds F . f = H1(f) from PBOOLE:sch_5(); A2: dom F = the carrier of (UPS (S,(T |^ X))) by PARTFUN1:def_2; A3: rng F c= the carrier of ((UPS (S,T)) |^ X) proof let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng F or g in the carrier of ((UPS (S,T)) |^ X) ) assume g in rng F ; ::_thesis: g in the carrier of ((UPS (S,T)) |^ X) then consider f being set such that A4: f in dom F and A5: g = F . f by FUNCT_1:def_3; reconsider f = f as directed-sups-preserving Function of S,(T |^ X) by A4, Def4; g = commute f by A1, A4, A5; then reconsider g = g as Function of X, the carrier of (UPS (S,T)) by Th39; A6: rng g c= the carrier of (UPS (S,T)) ; dom g = X by FUNCT_2:def_1; then g in Funcs (X, the carrier of (UPS (S,T))) by A6, FUNCT_2:def_2; hence g in the carrier of ((UPS (S,T)) |^ X) by YELLOW_1:28; ::_thesis: verum end; then reconsider F = F as Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) by A2, FUNCT_2:2; take F ; ::_thesis: ( F is commuting & F is isomorphic ) consider G being ManySortedSet of the carrier of ((UPS (S,T)) |^ X) such that A7: for f being Element of ((UPS (S,T)) |^ X) holds G . f = H1(f) from PBOOLE:sch_5(); A8: dom G = the carrier of ((UPS (S,T)) |^ X) by PARTFUN1:def_2; A9: rng G c= the carrier of (UPS (S,(T |^ X))) proof let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng G or g in the carrier of (UPS (S,(T |^ X))) ) assume g in rng G ; ::_thesis: g in the carrier of (UPS (S,(T |^ X))) then consider f being set such that A10: f in dom G and A11: g = G . f by FUNCT_1:def_3; the carrier of ((UPS (S,T)) |^ X) = Funcs (X, the carrier of (UPS (S,T))) by YELLOW_1:28; then reconsider f = f as Function of X, the carrier of (UPS (S,T)) by A10, FUNCT_2:66; g = commute f by A7, A10, A11; then g is directed-sups-preserving Function of S,(T |^ X) by Th40; hence g in the carrier of (UPS (S,(T |^ X))) by Def4; ::_thesis: verum end; then reconsider G = G as Function of ((UPS (S,T)) |^ X),(UPS (S,(T |^ X))) by A8, FUNCT_2:2; A12: G is commuting proof hereby :: according to WAYBEL27:def_3 ::_thesis: for f being Function st f in dom G holds G . f = commute f let x be set ; ::_thesis: ( x in dom G implies x is Function-yielding Function ) assume x in dom G ; ::_thesis: x is Function-yielding Function then x in Funcs (X, the carrier of (UPS (S,T))) by A8, YELLOW_1:28; then x is Function of X, the carrier of (UPS (S,T)) by FUNCT_2:66; hence x is Function-yielding Function ; ::_thesis: verum end; thus for f being Function st f in dom G holds G . f = commute f by A7, A8; ::_thesis: verum end; A13: the carrier of (T |^ X) = Funcs (X, the carrier of T) by YELLOW_1:28; UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; then A14: (UPS (S,T)) |^ X is full SubRelStr of (T |^ the carrier of S) |^ X by YELLOW16:39; A15: UPS (S,(T |^ X)) is full SubRelStr of (T |^ X) |^ the carrier of S by Def4; then A16: G is monotone by A12, A14, Th19; thus A17: F is commuting ::_thesis: F is isomorphic proof hereby :: according to WAYBEL27:def_3 ::_thesis: for f being Function st f in dom F holds F . f = commute f let x be set ; ::_thesis: ( x in dom F implies x is Function-yielding Function ) assume x in dom F ; ::_thesis: x is Function-yielding Function then x is Function of S,(T |^ X) by Def4; hence x is Function-yielding Function ; ::_thesis: verum end; thus for f being Function st f in dom F holds F . f = commute f by A1, A2; ::_thesis: verum end; then A18: F is monotone by A15, A14, Th19; the carrier of ((UPS (S,T)) |^ X) = Funcs (X, the carrier of (UPS (S,T))) by YELLOW_1:28; then the carrier of ((UPS (S,T)) |^ X) c= Funcs (X,(Funcs ( the carrier of S, the carrier of T))) by Th22, FUNCT_5:56; then A19: F * G = id ((UPS (S,T)) |^ X) by A2, A8, A9, A17, A12, Th3; the carrier of (UPS (S,(T |^ X))) c= Funcs ( the carrier of S, the carrier of (T |^ X)) by Th22; then G * F = id (UPS (S,(T |^ X))) by A2, A3, A8, A17, A12, A13, Th3; hence F is isomorphic by A19, A18, A16, YELLOW16:15; ::_thesis: verum end; theorem Th42: :: WAYBEL27:42 for X being non empty set for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic proof let X be non empty set ; ::_thesis: for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic let S, T be non empty Poset; ::_thesis: UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic consider F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) such that A1: ( F is commuting & F is isomorphic ) by Th41; take F ; :: according to WAYBEL_1:def_8 ::_thesis: F is isomorphic thus F is isomorphic by A1; ::_thesis: verum end; theorem :: WAYBEL27:43 for S, T being complete continuous LATTICE holds UPS (S,T) is continuous proof let S, T be complete continuous LATTICE; ::_thesis: UPS (S,T) is continuous consider X being non empty set , p being projection Function of (BoolePoset X),(BoolePoset X) such that A1: p is directed-sups-preserving and A2: T, Image p are_isomorphic by WAYBEL15:18; A3: (id S) * (id S) = id S by QUANTAL1:def_9; Image p is non empty complete Poset by A2, WAYBEL20:18; then UPS (S,T), UPS (S,(Image p)) are_isomorphic by A2, Th36; then A4: UPS (S,T), Image (UPS ((id S),p)) are_isomorphic by A1, Th37; set L = the Scott TopAugmentation of S; A5: InclPoset (sigma the Scott TopAugmentation of S) is continuous by WAYBEL14:36; A6: UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic by Th34; p * p = p by QUANTAL1:def_9; then (UPS ((id S),p)) * (UPS ((id S),p)) = UPS ((id S),p) by A3, A1, Th28; then UPS ((id S),p) is idempotent directed-sups-preserving Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by A1, Th30, QUANTAL1:def_9; then A7: UPS ((id S),p) is directed-sups-preserving projection Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by WAYBEL_1:def_13; BoolePoset X,(BoolePoset 1) |^ X are_isomorphic by Th18; then A8: UPS (S,(BoolePoset X)), UPS (S,((BoolePoset 1) |^ X)) are_isomorphic by Th36; RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then InclPoset (sigma S) is continuous by A5, YELLOW_9:52; then ( UPS (S,(BoolePoset 1)) is continuous & UPS (S,(BoolePoset 1)) is complete ) by A6, WAYBEL15:9, WAYBEL_1:6; then for x being Element of X holds (X --> (UPS (S,(BoolePoset 1)))) . x is complete continuous LATTICE by FUNCOP_1:7; then X -POS_prod (X --> (UPS (S,(BoolePoset 1)))) is continuous by WAYBEL20:33; then A9: (UPS (S,(BoolePoset 1))) |^ X is continuous by YELLOW_1:def_5; UPS (S,((BoolePoset 1) |^ X)),(UPS (S,(BoolePoset 1))) |^ X are_isomorphic by Th42; then UPS (S,(BoolePoset X)),(UPS (S,(BoolePoset 1))) |^ X are_isomorphic by A8, WAYBEL_1:7; then UPS (S,(BoolePoset X)) is continuous LATTICE by A9, WAYBEL15:9, WAYBEL_1:6; then Image (UPS ((id S),p)) is continuous by A7, WAYBEL15:15; hence UPS (S,T) is continuous by A4, WAYBEL15:9, WAYBEL_1:6; ::_thesis: verum end; theorem :: WAYBEL27:44 for S, T being complete algebraic LATTICE holds UPS (S,T) is algebraic proof let S, T be complete algebraic LATTICE; ::_thesis: UPS (S,T) is algebraic consider X being non empty set , p being closure Function of (BoolePoset X),(BoolePoset X) such that A1: p is directed-sups-preserving and A2: T, Image p are_isomorphic by WAYBEL13:35; now__::_thesis:_for_i_being_Element_of_(UPS_(S,(BoolePoset_X)))_holds_(id_(UPS_(S,(BoolePoset_X))))_._i_<=_(UPS_((id_S),p))_._i let i be Element of (UPS (S,(BoolePoset X))); ::_thesis: (id (UPS (S,(BoolePoset X)))) . i <= (UPS ((id S),p)) . i reconsider f = i as directed-sups-preserving Function of S,(BoolePoset X) by Def4; A3: (UPS ((id S),p)) . f = (p * f) * (id the carrier of S) by A1, Def5 .= p * f by FUNCT_2:17 ; A4: now__::_thesis:_for_s_being_Element_of_S_holds_i_._s_<=_((UPS_((id_S),p))_._i)_._s let s be Element of S; ::_thesis: i . s <= ((UPS ((id S),p)) . i) . s A5: id (BoolePoset X) <= p by WAYBEL_1:def_14; A6: (id (BoolePoset X)) . (i . s) = i . s by FUNCT_1:18; (p * f) . s = p . (f . s) by FUNCT_2:15; hence i . s <= ((UPS ((id S),p)) . i) . s by A5, A6, A3, YELLOW_2:9; ::_thesis: verum end; (id (UPS (S,(BoolePoset X)))) . i = i by FUNCT_1:18; hence (id (UPS (S,(BoolePoset X)))) . i <= (UPS ((id S),p)) . i by A4, Th23; ::_thesis: verum end; then A7: id (UPS (S,(BoolePoset X))) <= UPS ((id S),p) by YELLOW_2:9; A8: (id S) * (id S) = id S by QUANTAL1:def_9; p * p = p by QUANTAL1:def_9; then (UPS ((id S),p)) * (UPS ((id S),p)) = UPS ((id S),p) by A8, A1, Th28; then UPS ((id S),p) is idempotent directed-sups-preserving Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by A1, Th30, QUANTAL1:def_9; then UPS ((id S),p) is projection by WAYBEL_1:def_13; then reconsider Sp = UPS ((id S),p) as directed-sups-preserving closure Function of (UPS (S,(BoolePoset X))),(UPS (S,(BoolePoset X))) by A7, A1, Th30, WAYBEL_1:def_14; Image p is non empty complete Poset by A2, WAYBEL20:18; then UPS (S,T), UPS (S,(Image p)) are_isomorphic by A2, Th36; then A9: UPS (S,T), Image Sp are_isomorphic by A1, Th37; BoolePoset X,(BoolePoset 1) |^ X are_isomorphic by Th18; then A10: UPS (S,(BoolePoset X)), UPS (S,((BoolePoset 1) |^ X)) are_isomorphic by Th36; set L = the Scott TopAugmentation of S; A11: InclPoset (sigma S) = InclPoset the topology of the Scott TopAugmentation of S by YELLOW_9:51; A12: RelStr(# the carrier of the Scott TopAugmentation of S, the InternalRel of the Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def_4; then the Scott TopAugmentation of S is algebraic by WAYBEL13:26, WAYBEL13:32; then ex B being Basis of the Scott TopAugmentation of S st B = { (uparrow x) where x is Element of the Scott TopAugmentation of S : x in the carrier of (CompactSublatt the Scott TopAugmentation of S) } by WAYBEL14:42; then InclPoset (sigma the Scott TopAugmentation of S) is algebraic by WAYBEL14:43; then A13: InclPoset (sigma S) is algebraic by A12, YELLOW_9:52; UPS (S,(BoolePoset 1)), InclPoset (sigma S) are_isomorphic by Th34; then ( UPS (S,(BoolePoset 1)) is algebraic & UPS (S,(BoolePoset 1)) is lower-bounded ) by A13, A11, WAYBEL13:32, WAYBEL_1:6; then ( X -POS_prod (X --> (UPS (S,(BoolePoset 1)))) is lower-bounded & X -POS_prod (X --> (UPS (S,(BoolePoset 1)))) is algebraic ) ; then A14: ( (UPS (S,(BoolePoset 1))) |^ X is algebraic & (UPS (S,(BoolePoset 1))) |^ X is lower-bounded ) by YELLOW_1:def_5; UPS (S,((BoolePoset 1) |^ X)),(UPS (S,(BoolePoset 1))) |^ X are_isomorphic by Th42; then UPS (S,(BoolePoset X)),(UPS (S,(BoolePoset 1))) |^ X are_isomorphic by A10, WAYBEL_1:7; then UPS (S,(BoolePoset X)) is lower-bounded algebraic LATTICE by A14, WAYBEL13:32, WAYBEL_1:6; then A15: Image Sp is algebraic by WAYBEL_8:24; Image Sp is complete LATTICE by YELLOW_2:30; hence UPS (S,T) is algebraic by A9, A15, WAYBEL13:32, WAYBEL_1:6; ::_thesis: verum end; theorem Th45: :: WAYBEL27:45 for R, S, T being complete LATTICE for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T proof let R, S, T be complete LATTICE; ::_thesis: for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T let f be directed-sups-preserving Function of R,(UPS (S,T)); ::_thesis: uncurry f is directed-sups-preserving Function of [:R,S:],T A1: f in Funcs ( the carrier of R, the carrier of (UPS (S,T))) by FUNCT_2:8; Funcs ( the carrier of R, the carrier of (UPS (S,T))) c= Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by Th22, FUNCT_5:56; then uncurry f in Funcs ([: the carrier of R, the carrier of S:], the carrier of T) by A1, FUNCT_6:11; then uncurry f in Funcs ( the carrier of [:R,S:], the carrier of T) by YELLOW_3:def_2; then reconsider g = uncurry f as Function of [:R,S:],T by FUNCT_2:66; A2: the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T) by Th22; now__::_thesis:_for_a_being_Element_of_R for_b_being_Element_of_S_holds_ (_Proj_(g,a)_is_directed-sups-preserving_&_Proj_(g,b)_is_directed-sups-preserving_) reconsider ST = UPS (S,T) as non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def4, Th26; let a be Element of R; ::_thesis: for b being Element of S holds ( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving ) let b be Element of S; ::_thesis: ( Proj (g,a) is directed-sups-preserving & Proj (g,b) is directed-sups-preserving ) reconsider f9 = f as directed-sups-preserving Function of R,ST ; incl (ST,(T |^ the carrier of S)) is directed-sups-preserving by WAYBEL21:10; then A3: (incl (ST,(T |^ the carrier of S))) * f9 is directed-sups-preserving by WAYBEL20:28; the carrier of ST c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13; then incl (ST,(T |^ the carrier of S)) = id the carrier of ST by YELLOW_9:def_1; then f is directed-sups-preserving Function of R,(T |^ the carrier of S) by A3, FUNCT_2:17; then A4: (commute f) . b is directed-sups-preserving Function of R,T by Th38; rng f c= Funcs ( the carrier of S, the carrier of T) by A2, XBOOLE_1:1; then curry g = f by FUNCT_5:48; then Proj (g,a) = f . a by WAYBEL24:def_1; hence Proj (g,a) is directed-sups-preserving by Def4; ::_thesis: Proj (g,b) is directed-sups-preserving Proj (g,b) = (curry' g) . b by WAYBEL24:def_2; hence Proj (g,b) is directed-sups-preserving by A4, FUNCT_6:def_10; ::_thesis: verum end; hence uncurry f is directed-sups-preserving Function of [:R,S:],T by WAYBEL24:18; ::_thesis: verum end; theorem Th46: :: WAYBEL27:46 for R, S, T being complete LATTICE for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T)) proof let R, S, T be complete LATTICE; ::_thesis: for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T)) A1: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2; let f be directed-sups-preserving Function of [:R,S:],T; ::_thesis: curry f is directed-sups-preserving Function of R,(UPS (S,T)) A2: the carrier of (UPS ([:R,S:],T)) c= Funcs ( the carrier of [:R,S:], the carrier of T) by Th22; f in the carrier of (UPS ([:R,S:],T)) by Def4; then curry f in Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by A2, A1, FUNCT_6:10; then A3: curry f is Function of the carrier of R,(Funcs ( the carrier of S, the carrier of T)) by FUNCT_2:66; then A4: dom (curry f) = the carrier of R by FUNCT_2:def_1; rng (curry f) c= the carrier of (UPS (S,T)) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (curry f) or y in the carrier of (UPS (S,T)) ) assume y in rng (curry f) ; ::_thesis: y in the carrier of (UPS (S,T)) then consider x being set such that A5: x in dom (curry f) and A6: y = (curry f) . x by FUNCT_1:def_3; reconsider x = x as Element of R by A3, A5, FUNCT_2:def_1; Proj (f,x) is directed-sups-preserving by WAYBEL24:16; then y is directed-sups-preserving Function of S,T by A6, WAYBEL24:def_1; hence y in the carrier of (UPS (S,T)) by Def4; ::_thesis: verum end; then reconsider g = curry f as Function of R,(UPS (S,T)) by A4, FUNCT_2:2; A7: UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; A8: dom f = the carrier of [:R,S:] by FUNCT_2:def_1; g is directed-sups-preserving proof let A be Subset of R; :: according to WAYBEL_0:def_37 ::_thesis: ( A is empty or not A is directed or g preserves_sup_of A ) assume ( not A is empty & A is directed ) ; ::_thesis: g preserves_sup_of A then reconsider B = A as non empty directed Subset of R ; reconsider gsA = g . (sup A) as Element of (T |^ the carrier of S) by A7, YELLOW_0:58; assume ex_sup_of A,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of g .: A, UPS (S,T) & "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R)) ) thus ex_sup_of g .: A, UPS (S,T) by YELLOW_0:17; ::_thesis: "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R)) A9: for s being Element of S holds ( the carrier of S --> T) . s is complete LATTICE by FUNCOP_1:7; the carrier of (UPS (S,T)) c= the carrier of (T |^ the carrier of S) by A7, YELLOW_0:def_13; then g .: B c= the carrier of (T |^ the carrier of S) by XBOOLE_1:1; then reconsider gA = g .: A as non empty Subset of (T |^ the carrier of S) ; A10: T |^ the carrier of S = product ( the carrier of S --> T) by YELLOW_1:def_5; then A11: dom gsA = the carrier of S by WAYBEL_3:27; A12: dom gsA = the carrier of S by A10, WAYBEL_3:27; A13: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S_holds_ (sup_gA)_._x_=_gsA_._x let x be set ; ::_thesis: ( x in the carrier of S implies (sup gA) . x = gsA . x ) assume x in the carrier of S ; ::_thesis: (sup gA) . x = gsA . x then reconsider s = x as Element of S ; reconsider s1 = {s} as non empty directed Subset of S by WAYBEL_0:5; reconsider As = [:B,s1:] as non empty directed Subset of [:R,S:] ; A14: f preserves_sup_of As by WAYBEL_0:def_37; A15: ex_sup_of As,[:R,S:] by YELLOW_0:17; ( the carrier of S --> T) . s = T by FUNCOP_1:7; hence (sup gA) . x = sup (pi (gA,s)) by A9, A10, WAYBEL_3:32 .= sup (f .: As) by A8, Th9 .= f . (sup As) by A14, A15, WAYBEL_0:def_31 .= f . [(sup (proj1 As)),(sup (proj2 As))] by YELLOW_3:46 .= f . [(sup A),(sup (proj2 As))] by FUNCT_5:9 .= f . [(sup A),(sup {s})] by FUNCT_5:9 .= f . ((sup A),s) by YELLOW_0:39 .= gsA . x by A4, A12, FUNCT_5:31 ; ::_thesis: verum end; dom (sup gA) = the carrier of S by A10, WAYBEL_3:27; then sup gA = gsA by A13, A11, FUNCT_1:2; hence "\/" ((g .: A),(UPS (S,T))) = g . ("\/" (A,R)) by Th27; ::_thesis: verum end; hence curry f is directed-sups-preserving Function of R,(UPS (S,T)) ; ::_thesis: verum end; theorem :: WAYBEL27:47 for R, S, T being complete LATTICE ex f being Function of (UPS (R,(UPS (S,T)))),(UPS ([:R,S:],T)) st ( f is uncurrying & f is isomorphic ) proof deffunc H1( Function) -> set = uncurry \$1; let R, S, T be complete LATTICE; ::_thesis: ex f being Function of (UPS (R,(UPS (S,T)))),(UPS ([:R,S:],T)) st ( f is uncurrying & f is isomorphic ) consider F being ManySortedSet of the carrier of (UPS (R,(UPS (S,T)))) such that A1: for f being Element of (UPS (R,(UPS (S,T)))) holds F . f = H1(f) from PBOOLE:sch_5(); A2: dom F = the carrier of (UPS (R,(UPS (S,T)))) by PARTFUN1:def_2; A3: rng F c= the carrier of (UPS ([:R,S:],T)) proof let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng F or g in the carrier of (UPS ([:R,S:],T)) ) assume g in rng F ; ::_thesis: g in the carrier of (UPS ([:R,S:],T)) then consider f being set such that A4: f in dom F and A5: g = F . f by FUNCT_1:def_3; reconsider f = f as directed-sups-preserving Function of R,(UPS (S,T)) by A4, Def4; g = uncurry f by A1, A4, A5; then g is directed-sups-preserving Function of [:R,S:],T by Th45; hence g in the carrier of (UPS ([:R,S:],T)) by Def4; ::_thesis: verum end; then reconsider F = F as Function of (UPS (R,(UPS (S,T)))),(UPS ([:R,S:],T)) by A2, FUNCT_2:2; take F ; ::_thesis: ( F is uncurrying & F is isomorphic ) thus A6: F is uncurrying ::_thesis: F is isomorphic proof hereby :: according to WAYBEL27:def_1 ::_thesis: for f being Function st f in dom F holds F . f = uncurry f let x be set ; ::_thesis: ( x in dom F implies x is Function-yielding Function ) assume x in dom F ; ::_thesis: x is Function-yielding Function then x is Function of R,(UPS (S,T)) by Def4; hence x is Function-yielding Function ; ::_thesis: verum end; thus for f being Function st f in dom F holds F . f = uncurry f by A1, A2; ::_thesis: verum end; deffunc H2( Function) -> set = curry \$1; consider G being ManySortedSet of the carrier of (UPS ([:R,S:],T)) such that A7: for f being Element of (UPS ([:R,S:],T)) holds G . f = H2(f) from PBOOLE:sch_5(); A8: dom G = the carrier of (UPS ([:R,S:],T)) by PARTFUN1:def_2; A9: rng G c= the carrier of (UPS (R,(UPS (S,T)))) proof let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in rng G or g in the carrier of (UPS (R,(UPS (S,T)))) ) assume g in rng G ; ::_thesis: g in the carrier of (UPS (R,(UPS (S,T)))) then consider f being set such that A10: f in dom G and A11: g = G . f by FUNCT_1:def_3; reconsider f = f as directed-sups-preserving Function of [:R,S:],T by A10, Def4; g = curry f by A7, A10, A11; then g is directed-sups-preserving Function of R,(UPS (S,T)) by Th46; hence g in the carrier of (UPS (R,(UPS (S,T)))) by Def4; ::_thesis: verum end; then reconsider G = G as Function of (UPS ([:R,S:],T)),(UPS (R,(UPS (S,T)))) by A8, FUNCT_2:2; UPS (S,T) is full SubRelStr of T |^ the carrier of S by Def4; then A12: (UPS (S,T)) |^ the carrier of R is full SubRelStr of (T |^ the carrier of S) |^ the carrier of R by YELLOW16:39; UPS (R,(UPS (S,T))) is full SubRelStr of (UPS (S,T)) |^ the carrier of R by Def4; then A13: UPS (R,(UPS (S,T))) is non empty full SubRelStr of (T |^ the carrier of S) |^ the carrier of R by A12, YELLOW16:26; the carrier of [:R,S:] = [: the carrier of R, the carrier of S:] by YELLOW_3:def_2; then A14: UPS ([:R,S:],T) is non empty full SubRelStr of T |^ [: the carrier of R, the carrier of S:] by Def4; then A15: F is monotone by A6, A13, Th20; A16: G is currying proof hereby :: according to WAYBEL27:def_2 ::_thesis: for f being Function st f in dom G holds G . f = curry f let x be set ; ::_thesis: ( x in dom G implies ( x is Function & proj1 x is Relation ) ) assume x in dom G ; ::_thesis: ( x is Function & proj1 x is Relation ) then reconsider f = x as Function of [:R,S:],T by Def4; proj1 f = the carrier of [:R,S:] by FUNCT_2:def_1 .= [: the carrier of R, the carrier of S:] by YELLOW_3:def_2 ; hence ( x is Function & proj1 x is Relation ) ; ::_thesis: verum end; thus for f being Function st f in dom G holds G . f = curry f by A7, A8; ::_thesis: verum end; then A17: G is monotone by A13, A14, Th21; the carrier of ((T |^ the carrier of S) |^ the carrier of R) = Funcs ( the carrier of R, the carrier of (T |^ the carrier of S)) by YELLOW_1:28 .= Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by YELLOW_1:28 ; then the carrier of (UPS (R,(UPS (S,T)))) c= Funcs ( the carrier of R,(Funcs ( the carrier of S, the carrier of T))) by A13, YELLOW_0:def_13; then A18: G * F = id (UPS (R,(UPS (S,T)))) by A2, A3, A8, A6, A16, Th4; the carrier of (T |^ [: the carrier of R, the carrier of S:]) = Funcs ([: the carrier of R, the carrier of S:], the carrier of T) by YELLOW_1:28; then the carrier of (UPS ([:R,S:],T)) c= Funcs ([: the carrier of R, the carrier of S:], the carrier of T) by A14, YELLOW_0:def_13; then F * G = id (UPS ([:R,S:],T)) by A2, A8, A9, A6, A16, Th5; hence F is isomorphic by A18, A15, A17, YELLOW16:15; ::_thesis: verum end;