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