:: WAYBEL24 semantic presentation

begin

theorem :: WAYBEL24:1
for S, T being up-complete Scott TopLattice
for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T
proof
let S, T be up-complete Scott TopLattice; ::_thesis: for M being Subset of (SCMaps (S,T)) holds "\/" (M,(SCMaps (S,T))) is continuous Function of S,T
let M be Subset of (SCMaps (S,T)); ::_thesis: "\/" (M,(SCMaps (S,T))) is continuous Function of S,T
 the carrier of (SCMaps (S,T)) c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13;
then  "\/" (M,(SCMaps (S,T))) in the carrier of (MonMaps (S,T)) by TARSKI:def_3;
hence  "\/" (M,(SCMaps (S,T))) is continuous Function of S,T by WAYBEL10:9, WAYBEL17:def_2; ::_thesis: verum
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
cluster Function-like constant quasi_total  ->  monotone for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is constant holds
b1 is monotone
proof
let f be Function of S,T; ::_thesis: ( f is constant implies f is monotone )
assume A1: f is constant ; ::_thesis: f is monotone
 for x, y being Element of S st x <= y holds
f . x <= f . y
proof
let x, y be Element of S; ::_thesis: ( x <= y implies f . x <= f . y )
assume  x <= y ; ::_thesis: f . x <= f . y
 y in the carrier of S ;
then A2: y in dom f by FUNCT_2:def_1;
 x in the carrier of S ;
then  x in dom f by FUNCT_2:def_1;
hence  f . x <= f . y by A1, A2, FUNCT_1:def_10; ::_thesis: verum
end;
hence  f is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
let a be Element of T;
clusterS --> a ->  monotone ;
coherence
 S --> a is monotone
proof
set f = S --> a;
 for x, y being Element of S st x <= y holds
(S --> a) . x <= (S --> a) . y
proof
let x, y be Element of S; ::_thesis: ( x <= y implies (S --> a) . x <= (S --> a) . y )
assume  x <= y ; ::_thesis: (S --> a) . x <= (S --> a) . y
(S --> a) . x = ( the carrier of S --> a) . x
.= a by FUNCOP_1:7
.= ( the carrier of S --> a) . y by FUNCOP_1:7
.= (S --> a) . y ;
hence  (S --> a) . x <= (S --> a) . y ; ::_thesis: verum
end;
hence  S --> a is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;
end;

theorem :: WAYBEL24:2
for S being non empty RelStr
for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom (MonMaps (S,T)) = S --> (Bottom T)
let T be non empty reflexive antisymmetric lower-bounded RelStr ; ::_thesis: Bottom (MonMaps (S,T)) = S --> (Bottom T)
set L = MonMaps (S,T);
reconsider f = S --> (Bottom T) as Element of (MonMaps (S,T)) by WAYBEL10:9;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (MonMaps (S,T)) st b is_>=_than {} holds
f <= b
proof
let b be Element of (MonMaps (S,T)); ::_thesis: ( b is_>=_than {} implies f <= b )
assume  b is_>=_than {} ; ::_thesis: f <= b
reconsider b9 = b as Function of S,T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58;
 for x being Element of S holds f9 . x <= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x <= b9 . x
f9 . x = ( the carrier of S --> (Bottom T)) . x
.= Bottom T by FUNCOP_1:7 ;
hence  f9 . x <= b9 . x by YELLOW_0:44; ::_thesis: verum
end;
then  f9 <= b9 by YELLOW_2:9;
then  f99 <= b99 by WAYBEL10:11;
hence  f <= b by YELLOW_0:60; ::_thesis: verum
end;
 f is_>=_than {} by YELLOW_0:6;
then  f = "\/" ({},(MonMaps (S,T))) by A1, YELLOW_0:30;
hence  Bottom (MonMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum
end;

theorem :: WAYBEL24:3
for S being non empty RelStr
for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty reflexive antisymmetric upper-bounded RelStr holds Top (MonMaps (S,T)) = S --> (Top T)
let T be non empty reflexive antisymmetric upper-bounded RelStr ; ::_thesis: Top (MonMaps (S,T)) = S --> (Top T)
set L = MonMaps (S,T);
reconsider f = S --> (Top T) as Element of (MonMaps (S,T)) by WAYBEL10:9;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (MonMaps (S,T)) st b is_<=_than {} holds
f >= b
proof
let b be Element of (MonMaps (S,T)); ::_thesis: ( b is_<=_than {} implies f >= b )
assume  b is_<=_than {} ; ::_thesis: f >= b
reconsider b9 = b as Function of S,T by WAYBEL10:9;
reconsider b99 = b9, f99 = f as Element of (T |^ the carrier of S) by YELLOW_0:58;
 for x being Element of S holds f9 . x >= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x >= b9 . x
f9 . x = ( the carrier of S --> (Top T)) . x
.= Top T by FUNCOP_1:7 ;
hence  f9 . x >= b9 . x by YELLOW_0:45; ::_thesis: verum
end;
then  f9 >= b9 by YELLOW_2:9;
then  f99 >= b99 by WAYBEL10:11;
hence  f >= b by YELLOW_0:60; ::_thesis: verum
end;
 f is_<=_than {} by YELLOW_0:6;
then  f = "/\" ({},(MonMaps (S,T))) by A1, YELLOW_0:31;
hence  Top (MonMaps (S,T)) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum
end;

scheme :: WAYBEL24:sch 1
FuncFraenkelSL{ F1() ->  non empty RelStr , F2() ->  non empty RelStr , F3( set ) ->  Element of F2(), F4() ->  Function, P1[ set ] } :
 F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  =  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }
provided
A1: the carrier of F2() c= dom F4()
proof
set f = F4();
thus  F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  c=  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  c= F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  or y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  )
assume  y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  ; ::_thesis: y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }
then consider z being set  such that
 z in dom F4() and
A2: z in  {  F3(x) where x is Element of F1() : P1[x]  }  and
A3: y = F4() . z by FUNCT_1:def_6;
 ex x being Element of F1() st
( z = F3(x) & P1[x] ) by A2;
hence  y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  or y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  )
assume  y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  ; ::_thesis: y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }
then consider x being Element of F1() such that
A4: y = F4() . F3(x) and
A5: P1[x] ;
 ( F3(x) in the carrier of F2() & F3(x) in  {  F3(z) where z is Element of F1() : P1[z]  }  ) by A5;
hence  y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  by A1, A4, FUNCT_1:def_6; ::_thesis: verum
end;

scheme :: WAYBEL24:sch 2
Fraenkel6A{ F1() ->  LATTICE, F2( set ) ->  set , P1[ set ], P2[ set ] } :
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F2(v2) where v2 is Element of F1() : P2[v2]  }
provided
A1: for v being Element of F1() holds
( P1[v] iff P2[v] )
proof
thus   {  F2(v1) where v1 is Element of F1() : P1[v1]  }  c=  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  or a in  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  )
assume  a in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ; ::_thesis: a in  {  F2(v2) where v2 is Element of F1() : P2[v2]  }
then consider V1 being Element of F1() such that
A2: a = F2(V1) and
A3: P1[V1] ;
 P2[V1] by A1, A3;
hence  a in  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  by A2; ::_thesis: verum
end;
thus   {  F2(v2) where v2 is Element of F1() : P2[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  F2(v2) where v2 is Element of F1() : P2[v2]  }  or a in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  )
assume  a in  {  F2(v1) where v1 is Element of F1() : P2[v1]  }  ; ::_thesis: a in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
then consider V1 being Element of F1() such that
A4: a = F2(V1) and
A5: P2[V1] ;
 P1[V1] by A1, A5;
hence  a in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  by A4; ::_thesis: verum
end;
end;

theorem Th4: :: WAYBEL24:4
for S, T being complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))
proof
let S, T be complete LATTICE; ::_thesis: for f being monotone Function of S,T
for x being Element of S holds f . x = sup (f .: (downarrow x))
let f be monotone Function of S,T; ::_thesis: for x being Element of S holds f . x = sup (f .: (downarrow x))
let x be Element of S; ::_thesis: f . x = sup (f .: (downarrow x))
A1: for b being Element of T st b is_>=_than f .: (downarrow x) holds
f . x <= b
proof
let b be Element of T; ::_thesis: ( b is_>=_than f .: (downarrow x) implies f . x <= b )
 x <= x ;
then  ( dom f = the carrier of S & x in downarrow x ) by FUNCT_2:def_1, WAYBEL_0:17;
then A2: f . x in f .: (downarrow x) by FUNCT_1:def_6;
assume  b is_>=_than f .: (downarrow x) ; ::_thesis: f . x <= b
hence  f . x <= b by A2, LATTICE3:def_9; ::_thesis: verum
end;
 ( ex_sup_of downarrow x,S & sup (downarrow x) = x ) by WAYBEL_0:34;
then  downarrow x is_<=_than x by YELLOW_0:30;
then  f .: (downarrow x) is_<=_than f . x by YELLOW_2:14;
hence  f . x = sup (f .: (downarrow x)) by A1, YELLOW_0:30; ::_thesis: verum
end;

theorem :: WAYBEL24:5
for S, T being lower-bounded complete LATTICE
for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" ( {  (f . w) where w is Element of S : w <= x  }  ,T)
proof
let S, T be lower-bounded complete LATTICE; ::_thesis: for f being monotone Function of S,T
for x being Element of S holds f . x = "\/" ( {  (f . w) where w is Element of S : w <= x  }  ,T)
let f be monotone Function of S,T; ::_thesis: for x being Element of S holds f . x = "\/" ( {  (f . w) where w is Element of S : w <= x  }  ,T)
let x be Element of S; ::_thesis: f . x = "\/" ( {  (f . w) where w is Element of S : w <= x  }  ,T)
deffunc H1( Element of S) ->  Element of S = $1;
defpred S1[ Element of S] means $1 <= x;
defpred S2[ Element of S] means  ex y1 being Element of S st
( $1 <= y1 & y1 in {x} );
A1: the carrier of S c= dom f by FUNCT_2:def_1;
A2: f .:  {  H1(w) where w is Element of S : S1[w]  }  =  {  (f . H1(w)) where w is Element of S : S1[w]  }  from WAYBEL24:sch_1(A1);
A3: for x2 being Element of S holds
( S1[x2] iff S2[x2] )
proof
let x2 be Element of S; ::_thesis: ( S1[x2] iff S2[x2] )
hereby  ::_thesis: ( S2[x2] implies S1[x2] )
A4: x in {x} by TARSKI:def_1;
assume  x2 <= x ; ::_thesis: ex y1 being Element of S st
( x2 <= y1 & y1 in {x} )
hence  ex y1 being Element of S st
( x2 <= y1 & y1 in {x} ) by A4; ::_thesis: verum
end;
given y1 being Element of S such that A5: ( x2 <= y1 & y1 in {x} ) ; ::_thesis: S1[x2]
thus  S1[x2] by A5, TARSKI:def_1; ::_thesis: verum
end;
  {  H1(w) where w is Element of S : S1[w]  }  =  {  H1(x1) where x1 is Element of S : S2[x1]  }  from WAYBEL24:sch_2(A3);
then A6: downarrow x =  {  w where w is Element of S : w <= x  }  by WAYBEL_0:14;
sup (f .: (downarrow x)) = f . x by Th4
.= f . (sup (downarrow x)) by WAYBEL_0:34 ;
hence  f . x = "\/" ( {  (f . w) where w is Element of S : w <= x  }  ,T) by A2, A6, WAYBEL_0:34; ::_thesis: verum
end;

theorem Th6: :: WAYBEL24:6
for S being RelStr
for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
proof
let S be RelStr ; ::_thesis: for T being non empty RelStr
for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
let T be non empty RelStr ; ::_thesis: for F being Subset of (T |^ the carrier of S) holds sup F is Function of S,T
let F be Subset of (T |^ the carrier of S); ::_thesis: sup F is Function of S,T
set f = sup F;
 sup F in the carrier of (T |^ the carrier of S) ;
then  sup F in Funcs ( the carrier of S, the carrier of T) by YELLOW_1:28;
then  ex f9 being Function st
( f9 = sup F & dom f9 = the carrier of S & rng f9 c= the carrier of T ) by FUNCT_2:def_2;
hence  sup F is Function of S,T by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;

begin

definition
let X1, X2, Y be non empty RelStr ;
let f be Function of [:X1,X2:],Y;
let x be Element of X1;
func Proj (f,x) ->  Function of X2,Y equals :: WAYBEL24:def 1
(curry f) . x;
correctness
coherence
(curry f) . x is Function of X2,Y;
proof
 [: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def_2;
then  curry f is Function of the carrier of X1,(Funcs ( the carrier of X2, the carrier of Y)) by FUNCT_5:67;
hence  (curry f) . x is Function of X2,Y by FUNCT_2:5, FUNCT_2:66; ::_thesis: verum
end;
end;

:: deftheorem  defines Proj WAYBEL24:def_1_:_
 for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for x being Element of X1 holds Proj (f,x) = (curry f) . x;


theorem Th7: :: WAYBEL24:7
for Y, X1, X2 being non empty RelStr
for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
proof
let Y, X1, X2 be non empty RelStr ; ::_thesis: for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
let f be Function of [:X1,X2:],Y; ::_thesis: for x being Element of X1
for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
let x be Element of X1; ::_thesis: for y being Element of X2 holds (Proj (f,x)) . y = f . (x,y)
let y be Element of X2; ::_thesis: (Proj (f,x)) . y = f . (x,y)
dom f = the carrier of [:X1,X2:] by FUNCT_2:def_1
.= [: the carrier of X1, the carrier of X2:] by YELLOW_3:def_2 ;
then  [x,y] in dom f by ZFMISC_1:87;
hence  (Proj (f,x)) . y = f . (x,y) by FUNCT_5:20; ::_thesis: verum
end;

definition
let X1, X2, Y be non empty RelStr ;
let f be Function of [:X1,X2:],Y;
let y be Element of X2;
func Proj (f,y) ->  Function of X1,Y equals :: WAYBEL24:def 2
(curry' f) . y;
correctness
coherence
(curry' f) . y is Function of X1,Y;
proof
 [: the carrier of X1, the carrier of X2:] = the carrier of [:X1,X2:] by YELLOW_3:def_2;
then  curry' f is Function of the carrier of X2,(Funcs ( the carrier of X1, the carrier of Y)) by FUNCT_5:68;
hence  (curry' f) . y is Function of X1,Y by FUNCT_2:5, FUNCT_2:66; ::_thesis: verum
end;
end;

:: deftheorem  defines Proj WAYBEL24:def_2_:_
 for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2 holds Proj (f,y) = (curry' f) . y;

theorem Th8: :: WAYBEL24:8
for Y, X2, X1 being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
proof
let Y, X2, X1 be non empty RelStr ; ::_thesis: for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
let f be Function of [:X1,X2:],Y; ::_thesis: for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
let y be Element of X2; ::_thesis: for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)
let x be Element of X1; ::_thesis: (Proj (f,y)) . x = f . (x,y)
dom f = the carrier of [:X1,X2:] by FUNCT_2:def_1
.= [: the carrier of X1, the carrier of X2:] by YELLOW_3:def_2 ;
then  [x,y] in dom f by ZFMISC_1:87;
hence  (Proj (f,y)) . x = f . (x,y) by FUNCT_5:22; ::_thesis: verum
end;

theorem Th9: :: WAYBEL24:9
for R, S, T being non empty RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
proof
let R, S, T be non empty RelStr ; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let a be Element of R; ::_thesis: for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a
let b be Element of S; ::_thesis: (Proj (f,a)) . b = (Proj (f,b)) . a
(Proj (f,a)) . b = f . (a,b) by Th7
.= (Proj (f,b)) . a by Th8 ;
hence  (Proj (f,a)) . b = (Proj (f,b)) . a ; ::_thesis: verum
end;

registration
let S be non empty RelStr ;
let T be non empty reflexive RelStr ;
cluster non empty Relation-like the carrier of S -defined the carrier of T -valued Function-like V14( the carrier of S) quasi_total antitone for Element of bool [: the carrier of S, the carrier of T:];
existence
 ex b1 being Function of S,T st b1 is antitone
proof
set c = the Element of T;
take f = S --> the Element of T; ::_thesis: f is antitone
let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 ) )
assume  [x,y] in the InternalRel of S ; :: according to ORDERS_2:def_5 ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b2 <= b1 )
let a, b be Element of T; ::_thesis: ( not a = f . x or not b = f . y or b <= a )
assume that
A1: a = f . x and
A2: b = f . y ; ::_thesis: b <= a
 a = the Element of T by A1, FUNCOP_1:7;
hence  b <= a by A2, FUNCOP_1:7; ::_thesis: verum
end;
end;

theorem Th10: :: WAYBEL24:10
for R, S, T being non empty reflexive RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
proof
let R, S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
let a be Element of R; ::_thesis: for b being Element of S st f is monotone holds
( Proj (f,a) is monotone & Proj (f,b) is monotone )
let b be Element of S; ::_thesis: ( f is monotone implies ( Proj (f,a) is monotone & Proj (f,b) is monotone ) )
reconsider a = a as Element of R ;
reconsider b = b as Element of S ;
set g = Proj (f,b);
set h = Proj (f,a);
assume A1: f is monotone ; ::_thesis: ( Proj (f,a) is monotone & Proj (f,b) is monotone )
A2: now__::_thesis:_for_x,_y_being_Element_of_R_st_x_<=_y_holds_
(Proj_(f,b))_._x_<=_(Proj_(f,b))_._y
let x, y be Element of R; ::_thesis: ( x <= y implies (Proj (f,b)) . x <= (Proj (f,b)) . y )
A3: b <= b ;
A4: ( (Proj (f,b)) . x = f . (x,b) & (Proj (f,b)) . y = f . (y,b) ) by Th8;
assume  x <= y ; ::_thesis: (Proj (f,b)) . x <= (Proj (f,b)) . y
then  [x,b] <= [y,b] by A3, YELLOW_3:11;
hence  (Proj (f,b)) . x <= (Proj (f,b)) . y by A1, A4, WAYBEL_1:def_2; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
(Proj_(f,a))_._x_<=_(Proj_(f,a))_._y
let x, y be Element of S; ::_thesis: ( x <= y implies (Proj (f,a)) . x <= (Proj (f,a)) . y )
A5: a <= a ;
A6: ( (Proj (f,a)) . x = f . (a,x) & (Proj (f,a)) . y = f . (a,y) ) by Th7;
assume  x <= y ; ::_thesis: (Proj (f,a)) . x <= (Proj (f,a)) . y
then  [a,x] <= [a,y] by A5, YELLOW_3:11;
hence  (Proj (f,a)) . x <= (Proj (f,a)) . y by A1, A6, WAYBEL_1:def_2; ::_thesis: verum
end;
hence  ( Proj (f,a) is monotone & Proj (f,b) is monotone ) by A2, WAYBEL_1:def_2; ::_thesis: verum
end;

theorem Th11: :: WAYBEL24:11
for R, S, T being non empty reflexive RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
proof
let R, S, T be non empty reflexive RelStr ; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let a be Element of R; ::_thesis: for b being Element of S st f is antitone holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
let b be Element of S; ::_thesis: ( f is antitone implies ( Proj (f,a) is antitone & Proj (f,b) is antitone ) )
reconsider a9 = a as Element of R ;
set g = Proj (f,b);
set h = Proj (f,a);
assume A1: f is antitone ; ::_thesis: ( Proj (f,a) is antitone & Proj (f,b) is antitone )
A2: now__::_thesis:_for_x,_y_being_Element_of_R_st_x_<=_y_holds_
(Proj_(f,b))_._x_>=_(Proj_(f,b))_._y
reconsider b9 = b as Element of S ;
let x, y be Element of R; ::_thesis: ( x <= y implies (Proj (f,b)) . x >= (Proj (f,b)) . y )
A3: b9 <= b9 ;
A4: ( (Proj (f,b)) . x = f . (x,b) & (Proj (f,b)) . y = f . (y,b) ) by Th8;
assume  x <= y ; ::_thesis: (Proj (f,b)) . x >= (Proj (f,b)) . y
then  [x,b9] <= [y,b9] by A3, YELLOW_3:11;
hence  (Proj (f,b)) . x >= (Proj (f,b)) . y by A1, A4, WAYBEL_0:def_5; ::_thesis: verum
end;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
(Proj_(f,a))_._x_>=_(Proj_(f,a))_._y
let x, y be Element of S; ::_thesis: ( x <= y implies (Proj (f,a)) . x >= (Proj (f,a)) . y )
A5: a9 <= a9 ;
A6: ( (Proj (f,a)) . x = f . (a,x) & (Proj (f,a)) . y = f . (a,y) ) by Th7;
assume  x <= y ; ::_thesis: (Proj (f,a)) . x >= (Proj (f,a)) . y
then  [a9,x] <= [a9,y] by A5, YELLOW_3:11;
hence  (Proj (f,a)) . x >= (Proj (f,a)) . y by A1, A6, WAYBEL_0:def_5; ::_thesis: verum
end;
hence  ( Proj (f,a) is antitone & Proj (f,b) is antitone ) by A2, WAYBEL_9:def_1; ::_thesis: verum
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be monotone Function of [:R,S:],T;
let a be Element of R;
cluster Proj (f,a) ->  monotone ;
coherence
 Proj (f,a) is monotone by Th10;
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be monotone Function of [:R,S:],T;
let b be Element of S;
cluster Proj (f,b) ->  monotone ;
coherence
 Proj (f,b) is monotone by Th10;
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be antitone Function of [:R,S:],T;
let a be Element of R;
cluster Proj (f,a) ->  antitone ;
coherence
 Proj (f,a) is antitone by Th11;
end;

registration
let R, S, T be non empty reflexive RelStr ;
let f be antitone Function of [:R,S:],T;
let b be Element of S;
cluster Proj (f,b) ->  antitone ;
coherence
 Proj (f,b) is antitone by Th11;
end;

theorem Th12: :: WAYBEL24:12
for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds
f is monotone
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) holds
f is monotone
let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ) implies f is monotone )
assume A1: for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) ; ::_thesis: f is monotone
now__::_thesis:_for_x,_y_being_Element_of_[:R,S:]_st_x_<=_y_holds_
f_._x_<=_f_._y
let x, y be Element of [:R,S:]; ::_thesis: ( x <= y implies f . x <= f . y )
assume A2: x <= y ; ::_thesis: f . x <= f . y
then A3: x `1 <= y `1 by YELLOW_3:12;
A4: x `2 <= y `2 by A2, YELLOW_3:12;
A5: f . ((x `1),(y `2)) = (Proj (f,(x `1))) . (y `2) by Th7;
 ( Proj (f,(x `1)) is monotone & f . ((x `1),(x `2)) = (Proj (f,(x `1))) . (x `2) ) by A1, Th7;
then A6: f . [(x `1),(x `2)] <= f . [(x `1),(y `2)] by A4, A5, WAYBEL_1:def_2;
A7: f . ((y `1),(y `2)) = (Proj (f,(y `2))) . (y `1) by Th8;
 ( Proj (f,(y `2)) is monotone & f . ((x `1),(y `2)) = (Proj (f,(y `2))) . (x `1) ) by A1, Th8;
then  f . [(x `1),(y `2)] <= f . [(y `1),(y `2)] by A3, A7, WAYBEL_1:def_2;
then A8: f . [(x `1),(x `2)] <= f . [(y `1),(y `2)] by A6, YELLOW_0:def_2;
A9: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then  f . [(y `1),(y `2)] = f . y by MCART_1:21;
hence  f . x <= f . y by A8, A9, MCART_1:21; ::_thesis: verum
end;
hence  f is monotone by WAYBEL_1:def_2; ::_thesis: verum
end;

theorem :: WAYBEL24:13
for R, S, T being LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds
f is antitone
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds
f is antitone
let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) implies f is antitone )
assume A1: for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ; ::_thesis: f is antitone
now__::_thesis:_for_x,_y_being_Element_of_[:R,S:]_st_x_<=_y_holds_
f_._x_>=_f_._y
let x, y be Element of [:R,S:]; ::_thesis: ( x <= y implies f . x >= f . y )
assume A2: x <= y ; ::_thesis: f . x >= f . y
then A3: x `1 <= y `1 by YELLOW_3:12;
A4: x `2 <= y `2 by A2, YELLOW_3:12;
A5: f . ((x `1),(y `2)) = (Proj (f,(x `1))) . (y `2) by Th7;
 ( Proj (f,(x `1)) is antitone & f . ((x `1),(x `2)) = (Proj (f,(x `1))) . (x `2) ) by A1, Th7;
then A6: f . [(x `1),(x `2)] >= f . [(x `1),(y `2)] by A4, A5, WAYBEL_9:def_1;
A7: f . ((y `1),(y `2)) = (Proj (f,(y `2))) . (y `1) by Th8;
 ( Proj (f,(y `2)) is antitone & f . ((x `1),(y `2)) = (Proj (f,(y `2))) . (x `1) ) by A1, Th8;
then  f . [(x `1),(y `2)] >= f . [(y `1),(y `2)] by A3, A7, WAYBEL_9:def_1;
then A8: f . [(x `1),(x `2)] >= f . [(y `1),(y `2)] by A6, YELLOW_0:def_2;
A9: [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then  f . [(y `1),(y `2)] = f . y by MCART_1:21;
hence  f . x >= f . y by A8, A9, MCART_1:21; ::_thesis: verum
end;
hence  f is antitone by WAYBEL_9:def_1; ::_thesis: verum
end;

theorem Th14: :: WAYBEL24:14
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T
for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
let f be Function of [:R,S:],T; ::_thesis: for b being Element of S
for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
let b be Element of S; ::_thesis: for X being Subset of R holds (Proj (f,b)) .: X = f .: [:X,{b}:]
let X be Subset of R; ::_thesis: (Proj (f,b)) .: X = f .: [:X,{b}:]
A1: (Proj (f,b)) .: X c= f .: [:X,{b}:]
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in (Proj (f,b)) .: X or c in f .: [:X,{b}:] )
assume  c in (Proj (f,b)) .: X ; ::_thesis: c in f .: [:X,{b}:]
then consider k being set  such that
A2: k in dom (Proj (f,b)) and
A3: k in X and
A4: c = (Proj (f,b)) . k by FUNCT_1:def_6;
 b in {b} by TARSKI:def_1;
then A5: [k,b] in [:X,{b}:] by A3, ZFMISC_1:87;
 [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then  dom f = [: the carrier of R, the carrier of S:] by FUNCT_2:def_1;
then A6: [k,b] in dom f by A2, ZFMISC_1:87;
 c = f . (k,b) by A2, A4, Th8;
hence  c in f .: [:X,{b}:] by A5, A6, FUNCT_1:def_6; ::_thesis: verum
end;
 f .: [:X,{b}:] c= (Proj (f,b)) .: X
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in f .: [:X,{b}:] or c in (Proj (f,b)) .: X )
assume  c in f .: [:X,{b}:] ; ::_thesis: c in (Proj (f,b)) .: X
then consider k being set  such that
 k in dom f and
A7: k in [:X,{b}:] and
A8: c = f . k by FUNCT_1:def_6;
consider k1, k2 being set  such that
A9: k1 in X and
A10: k2 in {b} and
A11: k = [k1,k2] by A7, ZFMISC_1:def_2;
A12: k2 = b by A10, TARSKI:def_1;
 c = f . (k1,k2) by A8, A11;
then  ( dom (Proj (f,b)) = the carrier of R & c = (Proj (f,b)) . k1 ) by A9, A12, Th8, FUNCT_2:def_1;
hence  c in (Proj (f,b)) .: X by A9, FUNCT_1:def_6; ::_thesis: verum
end;
hence  (Proj (f,b)) .: X = f .: [:X,{b}:] by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th15: :: WAYBEL24:15
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T
for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let f be Function of [:R,S:],T; ::_thesis: for b being Element of R
for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let b be Element of R; ::_thesis: for X being Subset of S holds (Proj (f,b)) .: X = f .: [:{b},X:]
let X be Subset of S; ::_thesis: (Proj (f,b)) .: X = f .: [:{b},X:]
A1: (Proj (f,b)) .: X c= f .: [:{b},X:]
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in (Proj (f,b)) .: X or c in f .: [:{b},X:] )
assume  c in (Proj (f,b)) .: X ; ::_thesis: c in f .: [:{b},X:]
then consider k being set  such that
A2: k in dom (Proj (f,b)) and
A3: k in X and
A4: c = (Proj (f,b)) . k by FUNCT_1:def_6;
 b in {b} by TARSKI:def_1;
then A5: [b,k] in [:{b},X:] by A3, ZFMISC_1:87;
 [: the carrier of R, the carrier of S:] = the carrier of [:R,S:] by YELLOW_3:def_2;
then  dom f = [: the carrier of R, the carrier of S:] by FUNCT_2:def_1;
then A6: [b,k] in dom f by A2, ZFMISC_1:87;
 c = f . (b,k) by A2, A4, Th7;
hence  c in f .: [:{b},X:] by A5, A6, FUNCT_1:def_6; ::_thesis: verum
end;
 f .: [:{b},X:] c= (Proj (f,b)) .: X
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in f .: [:{b},X:] or c in (Proj (f,b)) .: X )
assume  c in f .: [:{b},X:] ; ::_thesis: c in (Proj (f,b)) .: X
then consider k being set  such that
 k in dom f and
A7: k in [:{b},X:] and
A8: c = f . k by FUNCT_1:def_6;
consider k1, k2 being set  such that
A9: k1 in {b} and
A10: k2 in X and
A11: k = [k1,k2] by A7, ZFMISC_1:def_2;
A12: k1 = b by A9, TARSKI:def_1;
 c = f . (k1,k2) by A8, A11;
then  ( dom (Proj (f,b)) = the carrier of S & c = (Proj (f,b)) . k2 ) by A10, A12, Th7, FUNCT_2:def_1;
hence  c in (Proj (f,b)) .: X by A10, FUNCT_1:def_6; ::_thesis: verum
end;
hence  (Proj (f,b)) .: X = f .: [:{b},X:] by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: WAYBEL24:16
for R, S, T being LATTICE
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
proof
let R, S, T be LATTICE; ::_thesis: for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let f be Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let a be Element of R; ::_thesis: for b being Element of S st f is directed-sups-preserving holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
let b be Element of S; ::_thesis: ( f is directed-sups-preserving implies ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) )
assume A1: f is directed-sups-preserving ; ::_thesis: ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving )
A2: for X being Subset of S st not X is empty & X is directed holds
Proj (f,a) preserves_sup_of X
proof
reconsider Y9 = {a} as non empty directed Subset of R by WAYBEL_0:5;
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies Proj (f,a) preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: Proj (f,a) preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
 Proj (f,a) preserves_sup_of X
proof
A3: sup Y9 = a by YELLOW_0:39;
A4: f preserves_sup_of [:Y9,X9:] by A1, WAYBEL_0:def_37;
A5: (Proj (f,a)) .: X = f .: [:Y9,X9:] by Th15;
A6: ex_sup_of Y9,R by YELLOW_0:38;
assume A7: ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) )
then A8: ex_sup_of [:Y9,X9:],[:R,S:] by A6, YELLOW_3:39;
sup ((Proj (f,a)) .: X) = sup (f .: [:Y9,X9:]) by Th15
.= f . (sup [:Y9,X9:]) by A8, A4, WAYBEL_0:def_31
.= f . ((sup Y9),(sup X9)) by A7, A6, YELLOW_3:43
.= (Proj (f,a)) . (sup X) by A3, Th7 ;
hence  ( ex_sup_of (Proj (f,a)) .: X,T & "\/" (((Proj (f,a)) .: X),T) = (Proj (f,a)) . ("\/" (X,S)) ) by A8, A4, A5, WAYBEL_0:def_31; ::_thesis: verum
end;
hence  Proj (f,a) preserves_sup_of X ; ::_thesis: verum
end;
 for X being Subset of R st not X is empty & X is directed holds
Proj (f,b) preserves_sup_of X
proof
reconsider Y9 = {b} as non empty directed Subset of S by WAYBEL_0:5;
let X be Subset of R; ::_thesis: ( not X is empty & X is directed implies Proj (f,b) preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: Proj (f,b) preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of R ;
 Proj (f,b) preserves_sup_of X
proof
A9: sup Y9 = b by YELLOW_0:39;
A10: f preserves_sup_of [:X9,Y9:] by A1, WAYBEL_0:def_37;
A11: (Proj (f,b)) .: X = f .: [:X9,Y9:] by Th14;
A12: ex_sup_of Y9,S by YELLOW_0:38;
assume A13: ex_sup_of X,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) )
then A14: ex_sup_of [:X9,Y9:],[:R,S:] by A12, YELLOW_3:39;
sup ((Proj (f,b)) .: X) = sup (f .: [:X9,Y9:]) by Th14
.= f . (sup [:X9,Y9:]) by A14, A10, WAYBEL_0:def_31
.= f . ((sup X9),(sup Y9)) by A13, A12, YELLOW_3:43
.= (Proj (f,b)) . (sup X) by A9, Th8 ;
hence  ( ex_sup_of (Proj (f,b)) .: X,T & "\/" (((Proj (f,b)) .: X),T) = (Proj (f,b)) . ("\/" (X,R)) ) by A14, A10, A11, WAYBEL_0:def_31; ::_thesis: verum
end;
hence  Proj (f,b) preserves_sup_of X ; ::_thesis: verum
end;
hence  ( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) by A2, WAYBEL_0:def_37; ::_thesis: verum
end;

theorem Th17: :: WAYBEL24:17
for R, S, T being LATTICE
for f being monotone Function of [:R,S:],T
for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
proof
let R, S, T be LATTICE; ::_thesis: for f being monotone Function of [:R,S:],T
for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let f be monotone Function of [:R,S:],T; ::_thesis: for a being Element of R
for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let a be Element of R; ::_thesis: for b being Element of S
for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let b be Element of S; ::_thesis: for X being directed Subset of [:R,S:] st ex_sup_of f .: X,T & a in proj1 X & b in proj2 X holds
f . [a,b] <= sup (f .: X)
let X be directed Subset of [:R,S:]; ::_thesis: ( ex_sup_of f .: X,T & a in proj1 X & b in proj2 X implies f . [a,b] <= sup (f .: X) )
assume that
A1: ex_sup_of f .: X,T and
A2: a in proj1 X and
A3: b in proj2 X ; ::_thesis: f . [a,b] <= sup (f .: X)
consider d being set  such that
A4: [d,b] in X by A3, XTUPLE_0:def_13;
 d in proj1 X by A4, XTUPLE_0:def_12;
then reconsider d = d as Element of R ;
consider c being set  such that
A5: [a,c] in X by A2, XTUPLE_0:def_12;
 c in proj2 X by A5, XTUPLE_0:def_13;
then reconsider c = c as Element of S ;
consider z being Element of [:R,S:] such that
A6: z in X and
A7: ( [a,c] <= z & [d,b] <= z ) by A5, A4, WAYBEL_0:def_1;
A8: f .: X is_<=_than sup (f .: X) by A1, YELLOW_0:30;
 [a,c] "\/" [d,b] <= z "\/" z by A7, YELLOW_3:3;
then  [a,c] "\/" [d,b] <= z by YELLOW_5:1;
then  [(a "\/" d),(c "\/" b)] <= z by YELLOW10:16;
then A9: f . [(a "\/" d),(c "\/" b)] <= f . z by WAYBEL_1:def_2;
 dom f = the carrier of [:R,S:] by FUNCT_2:def_1;
then  f . z in f .: X by A6, FUNCT_1:def_6;
then A10: f . z <= sup (f .: X) by A8, LATTICE3:def_9;
 ( a <= a "\/" d & b <= c "\/" b ) by YELLOW_0:22;
then  [a,b] <= [(a "\/" d),(c "\/" b)] by YELLOW_3:11;
then  f . [a,b] <= f . [(a "\/" d),(c "\/" b)] by WAYBEL_1:def_2;
then  f . [a,b] <= f . z by A9, YELLOW_0:def_2;
hence  f . [a,b] <= sup (f .: X) by A10, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: WAYBEL24:18
for R, S, T being complete LATTICE
for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds
f is directed-sups-preserving
proof
let R, S, T be complete LATTICE; ::_thesis: for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) holds
f is directed-sups-preserving
let f be Function of [:R,S:],T; ::_thesis: ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ) implies f is directed-sups-preserving )
assume A1: for a being Element of R
for b being Element of S holds
( Proj (f,a) is directed-sups-preserving & Proj (f,b) is directed-sups-preserving ) ; ::_thesis: f is directed-sups-preserving
 for X being Subset of [:R,S:] st not X is empty & X is directed holds
f preserves_sup_of X
proof
let X be Subset of [:R,S:]; ::_thesis: ( not X is empty & X is directed implies f preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: f preserves_sup_of X
then reconsider X = X as non empty directed Subset of [:R,S:] ;
 for a being Element of R
for b being Element of S holds
( Proj (f,a) is monotone & Proj (f,b) is monotone ) by A1, WAYBEL17:3;
then A2: f is monotone by Th12;
 f preserves_sup_of X
proof
 ( proj1 X is directed & not proj1 X is empty & Proj (f,("\/" ((proj2 X),S))) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22;
then A3: Proj (f,("\/" ((proj2 X),S))) preserves_sup_of proj1 X by WAYBEL_0:def_37;
A4: ex_sup_of (Proj (f,(sup (proj2 X)))) .: (proj1 X),T by YELLOW_0:17;
assume A5: ex_sup_of X,[:R,S:] ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) )
then A6: ex_sup_of proj1 X,R by YELLOW_3:41;
A7: ex_sup_of proj2 X,S by A5, YELLOW_3:41;
 for b being Element of T st b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) holds
b <= sup (f .: X)
proof
let b be Element of T; ::_thesis: ( b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) implies b <= sup (f .: X) )
assume  b in (Proj (f,(sup (proj2 X)))) .: (proj1 X) ; ::_thesis: b <= sup (f .: X)
then consider b1 being set  such that
A8: b1 in dom (Proj (f,(sup (proj2 X)))) and
A9: b1 in proj1 X and
A10: b = (Proj (f,(sup (proj2 X)))) . b1 by FUNCT_1:def_6;
reconsider b1 = b1 as Element of R by A8;
A11: (Proj (f,b1)) .: (proj2 X) is_<=_than sup (f .: X)
proof
let k be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not k in (Proj (f,b1)) .: (proj2 X) or k <= sup (f .: X) )
assume  k in (Proj (f,b1)) .: (proj2 X) ; ::_thesis: k <= sup (f .: X)
then consider k1 being set  such that
A12: k1 in dom (Proj (f,b1)) and
A13: k1 in proj2 X and
A14: k = (Proj (f,b1)) . k1 by FUNCT_1:def_6;
reconsider k1 = k1 as Element of S by A12;
 k = f . (b1,k1) by A14, Th7;
hence  k <= sup (f .: X) by A2, A9, A13, Th17, YELLOW_0:17; ::_thesis: verum
end;
 ( not proj2 X is empty & proj2 X is directed & Proj (f,b1) is directed-sups-preserving ) by A1, YELLOW_3:21, YELLOW_3:22;
then A15: Proj (f,b1) preserves_sup_of proj2 X by WAYBEL_0:def_37;
A16: ex_sup_of (Proj (f,b1)) .: (proj2 X),T by YELLOW_0:17;
b = (Proj (f,b1)) . (sup (proj2 X)) by A10, Th9
.= sup ((Proj (f,b1)) .: (proj2 X)) by A7, A15, WAYBEL_0:def_31 ;
hence  b <= sup (f .: X) by A16, A11, YELLOW_0:def_9; ::_thesis: verum
end;
then A17: (Proj (f,(sup (proj2 X)))) .: (proj1 X) is_<=_than sup (f .: X) by LATTICE3:def_9;
A18: sup (f .: X) <= f . (sup X) by A2, WAYBEL17:16;
f . (sup X) = f . ((sup (proj1 X)),(sup (proj2 X))) by YELLOW_3:46
.= (Proj (f,(sup (proj2 X)))) . (sup (proj1 X)) by Th8
.= sup ((Proj (f,(sup (proj2 X)))) .: (proj1 X)) by A6, A3, WAYBEL_0:def_31 ;
then  f . (sup X) <= sup (f .: X) by A17, A4, YELLOW_0:def_9;
hence  ( ex_sup_of f .: X,T & "\/" ((f .: X),T) = f . ("\/" (X,[:R,S:])) ) by A18, YELLOW_0:17, YELLOW_0:def_3; ::_thesis: verum
end;
hence  f preserves_sup_of X ; ::_thesis: verum
end;
hence  f is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum
end;

theorem Th19: :: WAYBEL24:19
for S being set
for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
proof
let S be set ; ::_thesis: for T being non empty RelStr
for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
let T be non empty RelStr ; ::_thesis: for f being set holds
( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
let f be set ; ::_thesis: ( f is Element of (T |^ S) iff f is Function of S, the carrier of T )
hereby  ::_thesis: ( f is Function of S, the carrier of T implies f is Element of (T |^ S) )
assume  f is Element of (T |^ S) ; ::_thesis: f is Function of S, the carrier of T
then  f in the carrier of (T |^ S) ;
then  f in Funcs (S, the carrier of T) by YELLOW_1:28;
then  ex a being Function st
( a = f & dom a = S & rng a c= the carrier of T ) by FUNCT_2:def_2;
hence  f is Function of S, the carrier of T by FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
assume  f is Function of S, the carrier of T ; ::_thesis: f is Element of (T |^ S)
then  f in Funcs (S, the carrier of T) by FUNCT_2:8;
hence  f is Element of (T |^ S) by YELLOW_1:28; ::_thesis: verum
end;

begin

definition
let S be TopStruct ;
let T be non empty TopRelStr ;
func ContMaps (S,T) ->  strict RelStr  means :Def3: :: WAYBEL24:def 3
( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of it iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) );
existence
 ex b1 being strict RelStr st
( b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) )
proof
defpred S1[ set ] means  ex f being Function of S,T st
( $1 = f & f is continuous );
consider X being set  such that
A1: for a being set holds
( a in X iff ( a in the carrier of (T |^ the carrier of S) & S1[a] ) ) from XBOOLE_0:sch_1();
 X c= the carrier of (T |^ the carrier of S)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in the carrier of (T |^ the carrier of S) )
assume  a in X ; ::_thesis: a in the carrier of (T |^ the carrier of S)
hence  a in the carrier of (T |^ the carrier of S) by A1; ::_thesis: verum
end;
then reconsider X = X as Subset of (T |^ the carrier of S) ;
take SX = subrelstr X; ::_thesis: ( SX is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of SX iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) )
thus  SX is full SubRelStr of T |^ the carrier of S ; ::_thesis: for x being set holds
( x in the carrier of SX iff ex f being Function of S,T st
( x = f & f is continuous ) )
let f be set ; ::_thesis: ( f in the carrier of SX iff ex f being Function of S,T st
( f = f & f is continuous ) )
hereby  ::_thesis: ( ex f being Function of S,T st
( f = f & f is continuous ) implies f in the carrier of SX )
assume  f in the carrier of SX ; ::_thesis: ex f9 being Function of S,T st
( f9 = f & f9 is continuous )
then  f in X by YELLOW_0:def_15;
then consider f9 being Function of S,T such that
A2: ( f9 = f & f9 is continuous ) by A1;
take f9 = f9; ::_thesis: ( f9 = f & f9 is continuous )
thus  ( f9 = f & f9 is continuous ) by A2; ::_thesis: verum
end;
given f9 being Function of S,T such that A3: f = f9 and
A4: f9 is continuous ; ::_thesis: f in the carrier of SX
 f in Funcs ( the carrier of S, the carrier of T) by A3, FUNCT_2:8;
then  f in the carrier of (T |^ the carrier of S) by YELLOW_1:28;
then  f in X by A1, A3, A4;
hence  f in the carrier of SX by YELLOW_0:def_15; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict RelStr st b1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) & b2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) holds
b1 = b2
proof
let A1, A2 be strict RelStr ; ::_thesis: ( A1 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) & A2 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of A2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) implies A1 = A2 )
assume that
A5: A1 is full SubRelStr of T |^ the carrier of S and
A6: for x being set holds
( x in the carrier of A1 iff ex f being Function of S,T st
( x = f & f is continuous ) ) and
A7: A2 is full SubRelStr of T |^ the carrier of S and
A8: for x being set holds
( x in the carrier of A2 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ; ::_thesis: A1 = A2
 the carrier of A1 = the carrier of A2
proof
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of A2 c= the carrier of A1
let x be set ; ::_thesis: ( x in the carrier of A1 implies x in the carrier of A2 )
assume  x in the carrier of A1 ; ::_thesis: x in the carrier of A2
then  ex f being Function of S,T st
( x = f & f is continuous ) by A6;
hence  x in the carrier of A2 by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A2 or x in the carrier of A1 )
assume  x in the carrier of A2 ; ::_thesis: x in the carrier of A1
then  ex f being Function of S,T st
( x = f & f is continuous ) by A8;
hence  x in the carrier of A1 by A6; ::_thesis: verum
end;
hence  A1 = A2 by A5, A7, YELLOW_0:57; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines ContMaps WAYBEL24:def_3_:_
 for S being TopStruct
for T being non empty TopRelStr
for b3 being strict RelStr holds
( b3 = ContMaps (S,T) iff ( b3 is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of b3 iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) ) );

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like TopRelStr ;
cluster ContMaps (S,T) ->  non empty strict ;
coherence
 not ContMaps (S,T) is empty
proof
set f = the continuous Function of S,T;
 the continuous Function of S,T in the carrier of (ContMaps (S,T)) by Def3;
hence  not ContMaps (S,T) is empty ; ::_thesis: verum
end;
end;

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like TopRelStr ;
cluster ContMaps (S,T) ->  constituted-Functions strict ;
coherence
 ContMaps (S,T) is constituted-Functions
proof
let a be Element of (ContMaps (S,T)); :: according to MONOID_0:def_1 ::_thesis: a is set
 ex a9 being Function of S,T st
( a9 = a & a9 is continuous ) by Def3;
hence  a is set ; ::_thesis: verum
end;
end;

theorem Th20: :: WAYBEL24:20
for S being non empty TopSpace
for T being non empty TopSpace-like reflexive TopRelStr
for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
proof
let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like reflexive TopRelStr
for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
let T be non empty TopSpace-like reflexive TopRelStr ; ::_thesis: for x, y being Element of (ContMaps (S,T)) holds
( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
let x, y be Element of (ContMaps (S,T)); ::_thesis: ( x <= y iff for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T )
A1: ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then reconsider x9 = x, y9 = y as Element of (T |^ the carrier of S) by YELLOW_0:58;
reconsider xa = x9, ya = y9 as Function of S,T by Th19;
hereby  ::_thesis: ( ( for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ) implies x <= y )
assume A2: x <= y ; ::_thesis: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T
let i be Element of S; ::_thesis: [(x . i),(y . i)] in the InternalRel of T
 x9 <= y9 by A1, A2, YELLOW_0:59;
then  xa <= ya by WAYBEL10:11;
then  ex a, b being Element of T st
( a = xa . i & b = ya . i & a <= b ) by YELLOW_2:def_1;
hence  [(x . i),(y . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
assume A3: for i being Element of S holds [(x . i),(y . i)] in the InternalRel of T ; ::_thesis: x <= y
now__::_thesis:_for_j_being_set_st_j_in_the_carrier_of_S_holds_
ex_a,_b_being_Element_of_T_st_
(_a_=_xa_._j_&_b_=_ya_._j_&_a_<=_b_)
let j be set ; ::_thesis: ( j in the carrier of S implies ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b ) )
assume  j in the carrier of S ; ::_thesis: ex a, b being Element of T st
( a = xa . j & b = ya . j & a <= b )
then reconsider i = j as Element of S ;
reconsider a = xa . i, b = ya . i as Element of T ;
take a = a; ::_thesis: ex b being Element of T st
( a = xa . j & b = ya . j & a <= b )
take b = b; ::_thesis: ( a = xa . j & b = ya . j & a <= b )
thus  ( a = xa . j & b = ya . j ) ; ::_thesis: a <= b
 [a,b] in the InternalRel of T by A3;
hence  a <= b by ORDERS_2:def_5; ::_thesis: verum
end;
then  xa <= ya by YELLOW_2:def_1;
then  x9 <= y9 by WAYBEL10:11;
hence  x <= y by A1, YELLOW_0:60; ::_thesis: verum
end;

theorem Th21: :: WAYBEL24:21
for S being non empty TopSpace
for T being non empty TopSpace-like reflexive TopRelStr
for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
proof
let S be non empty TopSpace; ::_thesis: for T being non empty TopSpace-like reflexive TopRelStr
for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
let T be non empty TopSpace-like reflexive TopRelStr ; ::_thesis: for x being set holds
( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
let x be set ; ::_thesis: ( x is continuous Function of S,T iff x is Element of (ContMaps (S,T)) )
thus  ( x is continuous Function of S,T implies x is Element of (ContMaps (S,T)) ) by Def3; ::_thesis: ( x is Element of (ContMaps (S,T)) implies x is continuous Function of S,T )
assume  x is Element of (ContMaps (S,T)) ; ::_thesis: x is continuous Function of S,T
then  ex f being Function of S,T st
( x = f & f is continuous ) by Def3;
hence  x is continuous Function of S,T ; ::_thesis: verum
end;

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like reflexive TopRelStr ;
cluster ContMaps (S,T) ->  strict reflexive ;
coherence
 ContMaps (S,T) is reflexive
proof
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
 CS is reflexive ;
hence  ContMaps (S,T) is reflexive ; ::_thesis: verum
end;
end;

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like transitive TopRelStr ;
cluster ContMaps (S,T) ->  strict transitive ;
coherence
 ContMaps (S,T) is transitive
proof
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
 CS is transitive ;
hence  ContMaps (S,T) is transitive ; ::_thesis: verum
end;
end;

registration
let S be non empty TopSpace;
let T be non empty TopSpace-like antisymmetric TopRelStr ;
cluster ContMaps (S,T) ->  strict antisymmetric ;
coherence
 ContMaps (S,T) is antisymmetric
proof
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
 CS is antisymmetric ;
hence  ContMaps (S,T) is antisymmetric ; ::_thesis: verum
end;
end;

registration
let S be set ;
let T be non empty RelStr ;
clusterT |^ S ->  constituted-Functions ;
coherence
 T |^ S is constituted-Functions
proof
let a be Element of (T |^ S); :: according to MONOID_0:def_1 ::_thesis: a is set
thus  a is set by Th19; ::_thesis: verum
end;
end;

theorem :: WAYBEL24:22
for S being non empty 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
proof
let S be non empty 1-sorted ; ::_thesis: for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
let T be complete LATTICE; ::_thesis: for f, g, h being Function of S,T
for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
let f, g, h be Function of S,T; ::_thesis: for i being Element of S st h = "\/" ({f,g},(T |^ the carrier of S)) holds
h . i = sup {(f . i),(g . i)}
let i be Element of S; ::_thesis: ( h = "\/" ({f,g},(T |^ the carrier of S)) implies h . i = sup {(f . i),(g . i)} )
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7;
reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def_5;
reconsider DU = {f9,g9} as Subset of (product SYT) ;
assume  h = "\/" ({f,g},(T |^ the carrier of S)) ; ::_thesis: h . i = sup {(f . i),(g . i)}
then h . i = (sup DU) . i by YELLOW_1:def_5
.= "\/" ((pi ({f,g},i)),(SYT . i)) by A1, WAYBEL_3:32
.= "\/" ((pi ({f,g},i)),T) by FUNCOP_1:7
.= sup {(f . i),(g . i)} by CARD_3:15 ;
hence  h . i = sup {(f . i),(g . i)} ; ::_thesis: verum
end;

theorem Th23: :: WAYBEL24:23
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
proof
let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds
for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete LATTICE ) implies for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i)) )
assume A1: for i being Element of I holds J . i is complete LATTICE ; ::_thesis: for X being Subset of (product J)
for i being Element of I holds (inf X) . i = inf (pi (X,i))
then reconsider L = product J as complete LATTICE by WAYBEL_3:31;
let X be Subset of (product J); ::_thesis: for i being Element of I holds (inf X) . i = inf (pi (X,i))
let i be Element of I; ::_thesis: (inf X) . i = inf (pi (X,i))
A2: L is complete ;
then A3: inf X is_<=_than X by YELLOW_0:33;
A4: (inf X) . i is_<=_than pi (X,i)
proof
let a be Element of (J . i); :: according to LATTICE3:def_8 ::_thesis: ( not a in pi (X,i) or (inf X) . i <= a )
assume  a in pi (X,i) ; ::_thesis: (inf X) . i <= a
then consider f being Function such that
A5: f in X and
A6: a = f . i by CARD_3:def_6;
reconsider f = f as Element of (product J) by A5;
 inf X <= f by A3, A5, LATTICE3:def_8;
hence  (inf X) . i <= a by A6, WAYBEL_3:28; ::_thesis: verum
end;
A7: now__::_thesis:_for_a_being_Element_of_(J_._i)_st_a_is_<=_than_pi_(X,i)_holds_
(inf_X)_._i_>=_a
let a be Element of (J . i); ::_thesis: ( a is_<=_than pi (X,i) implies (inf X) . i >= a )
set f = (inf X) +* (i,a);
A8: dom ((inf X) +* (i,a)) = dom (inf X) by FUNCT_7:30;
A9: dom (inf X) = I by WAYBEL_3:27;
now__::_thesis:_for_j_being_Element_of_I_holds_((inf_X)_+*_(i,a))_._j_is_Element_of_(J_._j)
let j be Element of I; ::_thesis: ((inf X) +* (i,a)) . j is Element of (J . j)
 ( j = i or j <> i ) ;
then  ( ((inf X) +* (i,a)) . j = (inf X) . j or ( ((inf X) +* (i,a)) . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32;
hence  ((inf X) +* (i,a)) . j is Element of (J . j) ; ::_thesis: verum
end;
then reconsider f = (inf X) +* (i,a) as Element of (product J) by A8, WAYBEL_3:27;
assume A10: a is_<=_than pi (X,i) ; ::_thesis: (inf X) . i >= a
 f is_<=_than X
proof
let g be Element of (product J); :: according to LATTICE3:def_8 ::_thesis: ( not g in X or f <= g )
assume  g in X ; ::_thesis: f <= g
then A11: ( g >= inf X & g . i in pi (X,i) ) by A2, CARD_3:def_6, YELLOW_2:22;
now__::_thesis:_for_j_being_Element_of_I_holds_f_._j_<=_g_._j
let j be Element of I; ::_thesis: f . j <= g . j
 ( j = i or j <> i ) ;
then  ( f . j = (inf X) . j or ( f . j = a & j = i ) ) by A9, FUNCT_7:31, FUNCT_7:32;
hence  f . j <= g . j by A10, A11, LATTICE3:def_8, WAYBEL_3:28; ::_thesis: verum
end;
hence  f <= g by WAYBEL_3:28; ::_thesis: verum
end;
then A12: f <= inf X by A2, YELLOW_0:33;
 f . i = a by A9, FUNCT_7:31;
hence  (inf X) . i >= a by A12, WAYBEL_3:28; ::_thesis: verum
end;
 J . i is complete LATTICE by A1;
hence  (inf X) . i = inf (pi (X,i)) by A4, A7, YELLOW_0:33; ::_thesis: verum
end;

theorem :: WAYBEL24:24
for S being non empty 1-sorted
for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
proof
let S be non empty 1-sorted ; ::_thesis: for T being complete LATTICE
for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let T be complete LATTICE; ::_thesis: for f, g, h being Function of S,T
for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let f, g, h be Function of S,T; ::_thesis: for i being Element of S st h = "/\" ({f,g},(T |^ the carrier of S)) holds
h . i = inf {(f . i),(g . i)}
let i be Element of S; ::_thesis: ( h = "/\" ({f,g},(T |^ the carrier of S)) implies h . i = inf {(f . i),(g . i)} )
reconsider f9 = f, g9 = g as Element of (T |^ the carrier of S) by Th19;
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
A1: for i being Element of S holds SYT . i is complete LATTICE by FUNCOP_1:7;
reconsider f9 = f9, g9 = g9 as Element of (product SYT) by YELLOW_1:def_5;
reconsider DU = {f9,g9} as Subset of (product SYT) ;
assume  h = "/\" ({f,g},(T |^ the carrier of S)) ; ::_thesis: h . i = inf {(f . i),(g . i)}
then h . i = (inf DU) . i by YELLOW_1:def_5
.= "/\" ((pi ({f,g},i)),(SYT . i)) by A1, Th23
.= "/\" ((pi ({f,g},i)),T) by FUNCOP_1:7
.= inf {(f . i),(g . i)} by CARD_3:15 ;
hence  h . i = inf {(f . i),(g . i)} ; ::_thesis: verum
end;

theorem Th25: :: WAYBEL24:25
for S being non empty RelStr
for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
proof
let S be non empty RelStr ; ::_thesis: for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
let T be complete LATTICE; ::_thesis: for F being non empty Subset of (T |^ the carrier of S)
for i being Element of S holds (sup F) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
let F be non empty Subset of (T |^ the carrier of S); ::_thesis: for i being Element of S holds (sup F) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
let i be Element of S; ::_thesis: (sup F) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
reconsider X = F as Subset of (product SYT) by YELLOW_1:def_5;
A1: pi (X,i) =  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }
proof
thus  pi (X,i) c=  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  c= pi (X,i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (X,i) or a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  )
assume  a in pi (X,i) ; ::_thesis: a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }
then  ex g being Function st
( g in X & a = g . i ) by CARD_3:def_6;
hence  a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ; ::_thesis: verum
end;
thus   {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  c= pi (X,i) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  or a in pi (X,i) )
assume  a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ; ::_thesis: a in pi (X,i)
then  ex g being Element of (T |^ the carrier of S) st
( a = g . i & g in F ) ;
hence  a in pi (X,i) by CARD_3:def_6; ::_thesis: verum
end;
end;
 ( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def_5;
then (sup F) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32
.= "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) by A1, FUNCOP_1:7 ;
hence  (sup F) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) ; ::_thesis: verum
end;

theorem Th26: :: WAYBEL24:26
for S, T being complete TopLattice
for F being non empty Subset of (ContMaps (S,T))
for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
proof
let S, T be complete TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
let i be Element of S; ::_thesis: ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)
reconsider SYT = the carrier of S --> T as RelStr-yielding non-Empty ManySortedSet of the carrier of S ;
reconsider SYT = SYT as RelStr-yielding non-Empty reflexive-yielding ManySortedSet of the carrier of S ;
 ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then  the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then A1: F c= the carrier of (T |^ the carrier of S) by XBOOLE_1:1;
then reconsider X = F as Subset of (product SYT) by YELLOW_1:def_5;
A2: pi (X,i) =  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }
proof
thus  pi (X,i) c=  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  c= pi (X,i)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (X,i) or a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  )
assume  a in pi (X,i) ; ::_thesis: a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }
then  ex g being Function st
( g in X & a = g . i ) by CARD_3:def_6;
hence  a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  by A1; ::_thesis: verum
end;
thus   {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  c= pi (X,i) ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  or a in pi (X,i) )
assume  a in  {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ; ::_thesis: a in pi (X,i)
then  ex g being Element of (T |^ the carrier of S) st
( a = g . i & g in F ) ;
hence  a in pi (X,i) by CARD_3:def_6; ::_thesis: verum
end;
end;
 ( T |^ the carrier of S = product SYT & ( for i being Element of S holds SYT . i is complete LATTICE ) ) by FUNCOP_1:7, YELLOW_1:def_5;
then ("\/" (F,(T |^ the carrier of S))) . i = "\/" ((pi (X,i)),(SYT . i)) by WAYBEL_3:32
.= "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) by A2, FUNCOP_1:7 ;
hence  ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) ; ::_thesis: verum
end;


theorem Th27: :: WAYBEL24:27
for S being non empty RelStr
for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
proof
let S be non empty RelStr ; ::_thesis: for T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
let T be complete LATTICE; ::_thesis: for F being non empty Subset of (T |^ the carrier of S)
for D being non empty Subset of S holds (sup F) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
let F be non empty Subset of (T |^ the carrier of S); ::_thesis: for D being non empty Subset of S holds (sup F) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
let D be non empty Subset of S; ::_thesis: (sup F) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
thus  (sup F) .: D c=  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  c= (sup F) .: D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (sup F) .: D or a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  )
assume  a in (sup F) .: D ; ::_thesis: a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
then consider x being set  such that
 x in dom (sup F) and
A1: x in D and
A2: a = (sup F) . x by FUNCT_1:def_6;
reconsider x9 = x as Element of S by A1;
 a = "\/" ( {  (f . x9) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) by A2, Th25;
hence  a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  by A1; ::_thesis: verum
end;
thus   {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  c= (sup F) .: D ::_thesis: verum
proof
 sup F is Function of S,T by Th6;
then A3: dom (sup F) = the carrier of S by FUNCT_2:def_1;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  or a in (sup F) .: D )
assume  a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  ; ::_thesis: a in (sup F) .: D
then consider i1 being Element of S such that
A4: ( a = "\/" ( {  (f . i1) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) & i1 in D ) ;
 a = (sup F) . i1 by A4, Th25;
hence  a in (sup F) .: D by A4, A3, FUNCT_1:def_6; ::_thesis: verum
end;
end;

theorem Th28: :: WAYBEL24:28
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty Subset of S holds ("\/" (F,(T |^ the carrier of S))) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
let D be non empty Subset of S; ::_thesis: ("\/" (F,(T |^ the carrier of S))) .: D =  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
thus  ("\/" (F,(T |^ the carrier of S))) .: D c=  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  c= ("\/" (F,(T |^ the carrier of S))) .: D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ("\/" (F,(T |^ the carrier of S))) .: D or a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  )
assume  a in ("\/" (F,(T |^ the carrier of S))) .: D ; ::_thesis: a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }
then consider x being set  such that
 x in dom ("\/" (F,(T |^ the carrier of S))) and
A1: x in D and
A2: a = ("\/" (F,(T |^ the carrier of S))) . x by FUNCT_1:def_6;
reconsider x9 = x as Element of S by A1;
 a = "\/" ( {  (f . x9) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) by A2, Th26;
hence  a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  by A1; ::_thesis: verum
end;
thus   {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  c= ("\/" (F,(T |^ the carrier of S))) .: D ::_thesis: verum
proof
 "\/" (F,(T |^ the carrier of S)) is Function of S,T by Th19;
then A3: dom ("\/" (F,(T |^ the carrier of S))) = the carrier of S by FUNCT_2:def_1;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  or a in ("\/" (F,(T |^ the carrier of S))) .: D )
assume  a in  {  ("\/" ( {  (f . i) where f is Element of (T |^ the carrier of S) : f in F  }  ,T)) where i is Element of S : i in D  }  ; ::_thesis: a in ("\/" (F,(T |^ the carrier of S))) .: D
then consider i1 being Element of S such that
A4: ( a = "\/" ( {  (f . i1) where f is Element of (T |^ the carrier of S) : f in F  }  ,T) & i1 in D ) ;
 a = ("\/" (F,(T |^ the carrier of S))) . i1 by A4, Th26;
hence  a in ("\/" (F,(T |^ the carrier of S))) .: D by A4, A3, FUNCT_1:def_6; ::_thesis: verum
end;
end;

scheme :: WAYBEL24:sch 3
FraenkelF9RS{ F1() ->  non empty TopRelStr , F2( set ) ->  set , F3( set ) ->  set , P1[ set ] } :
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proof
set X =  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ;
set Y =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ;
A2:  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  or x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  )
assume  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ; ::_thesis: x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
 x = F2(v1) by A1, A3, A4;
hence  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  by A4; ::_thesis: verum
end;
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  c=  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  or x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  )
assume  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ; ::_thesis: x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
 x = F3(v1) by A1, A5, A6;
hence  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A6; ::_thesis: verum
end;
hence   {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

scheme :: WAYBEL24:sch 4
FraenkelF9RSS{ F1() ->  non empty RelStr , F2( set ) ->  set , F3( set ) ->  set , P1[ set ] } :
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
provided
A1: for v being Element of F1() st P1[v] holds
F2(v) = F3(v)
proof
set X =  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ;
set Y =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ;
A2:  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  c=  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  or x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  )
assume  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  ; ::_thesis: x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }
then consider v1 being Element of F1() such that
A3: x = F3(v1) and
A4: P1[v1] ;
 x = F2(v1) by A1, A3, A4;
hence  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  by A4; ::_thesis: verum
end;
  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  c=  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  or x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  )
assume  x in  {  F2(v1) where v1 is Element of F1() : P1[v1]  }  ; ::_thesis: x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }
then consider v1 being Element of F1() such that
A5: x = F2(v1) and
A6: P1[v1] ;
 x = F3(v1) by A1, A5, A6;
hence  x in  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A6; ::_thesis: verum
end;
hence   {  F2(v1) where v1 is Element of F1() : P1[v1]  }  =  {  F3(v2) where v2 is Element of F1() : P1[v2]  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

scheme :: WAYBEL24:sch 5
FuncFraenkelS{ F1() ->  non empty TopRelStr , F2() ->  non empty TopRelStr , F3( set ) ->  Element of F2(), F4() ->  Function, P1[ set ] } :
 F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  =  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }
provided
A1: the carrier of F2() c= dom F4()
proof
set f = F4();
thus  F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  c=  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  c= F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  or y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  )
assume  y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  ; ::_thesis: y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }
then consider z being set  such that
 z in dom F4() and
A2: z in  {  F3(x) where x is Element of F1() : P1[x]  }  and
A3: y = F4() . z by FUNCT_1:def_6;
 ex x being Element of F1() st
( z = F3(x) & P1[x] ) by A2;
hence  y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  or y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  )
assume  y in  {  (F4() . F3(x)) where x is Element of F1() : P1[x]  }  ; ::_thesis: y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }
then consider x being Element of F1() such that
A4: y = F4() . F3(x) and
A5: P1[x] ;
 ( F3(x) in the carrier of F2() & F3(x) in  {  F3(z) where z is Element of F1() : P1[z]  }  ) by A5;
hence  y in F4() .:  {  F3(x) where x is Element of F1() : P1[x]  }  by A1, A4, FUNCT_1:def_6; ::_thesis: verum
end;

Lm1:  for S being non empty RelStr
for D being non empty Subset of S holds D =  {  i where i is Element of S : i in D  }
proof
let S be non empty RelStr ; ::_thesis: for D being non empty Subset of S holds D =  {  i where i is Element of S : i in D  }
let D be non empty Subset of S; ::_thesis: D =  {  i where i is Element of S : i in D  }
thus  D c=  {  i where i is Element of S : i in D  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  i where i is Element of S : i in D  }  c= D
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in  {  i where i is Element of S : i in D  }  )
assume  a in D ; ::_thesis: a in  {  i where i is Element of S : i in D  }
hence  a in  {  i where i is Element of S : i in D  }  ; ::_thesis: verum
end;
thus   {  i where i is Element of S : i in D  }  c= D ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  i where i is Element of S : i in D  }  or a in D )
assume  a in  {  i where i is Element of S : i in D  }  ; ::_thesis: a in D
then  ex j being Element of S st
( j = a & j in D ) ;
hence  a in D ; ::_thesis: verum
end;
end;

theorem Th29: :: WAYBEL24:29
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T
 ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then  the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then reconsider F9 = F as Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F9 as Function of S,T by Th6;
now__::_thesis:_for_x,_y_being_Element_of_S_st_x_<=_y_holds_
sF_._x_<=_sF_._y
let x, y be Element of S; ::_thesis: ( x <= y implies sF . x <= sF . y )
set G1 =  {  (f . x) where f is Element of (T |^ the carrier of S) : f in F9  }  ;
assume A1: x <= y ; ::_thesis: sF . x <= sF . y
A2:  {  (f . x) where f is Element of (T |^ the carrier of S) : f in F9  }  is_<=_than sF . y
proof
let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in  {  (f . x) where f is Element of (T |^ the carrier of S) : f in F9  }  or a <= sF . y )
assume  a in  {  (f . x) where f is Element of (T |^ the carrier of S) : f in F9  }  ; ::_thesis: a <= sF . y
then consider f9 being Element of (T |^ the carrier of S) such that
A3: a = f9 . x and
A4: f9 in F9 ;
reconsider f1 = f9 as continuous Function of S,T by A4, Th21;
reconsider f1 = f1 as monotone Function of S,T ;
 f9 <= sup F9 by A4, YELLOW_2:22;
then  f1 <= sF by WAYBEL10:11;
then A5: f1 . y <= sF . y by YELLOW_2:9;
 f1 . x <= f1 . y by A1, WAYBEL_1:def_2;
hence  a <= sF . y by A3, A5, YELLOW_0:def_2; ::_thesis: verum
end;
 sF . x = "\/" ( {  (f . x) where f is Element of (T |^ the carrier of S) : f in F9  }  ,T) by Th25;
hence  sF . x <= sF . y by A2, YELLOW_0:32; ::_thesis: verum
end;
hence  "\/" (F,(T |^ the carrier of S)) is monotone Function of S,T by WAYBEL_1:def_2; ::_thesis: verum
end;

theorem Th30: :: WAYBEL24:30
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T) = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T)
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T) = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T)
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty directed Subset of S holds "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T) = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T)
let D be non empty directed Subset of S; ::_thesis: "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T) = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T)
reconsider sF = "\/" (F,(T |^ the carrier of S)) as Function of S,T by Th19;
set F9 = F;
set L = "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T);
set P = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T);
set L1 =  {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ;
set P1 =  {  ("\/" ( {  (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F  }  ,T)) where i3 is Element of S : i3 in D  }  ;
reconsider L = "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T), P = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T) as Element of T ;
defpred S1[ set ] means $1 in F;
deffunc H1( Element of S) ->  Element of S = $1;
defpred S2[ set ] means $1 in D;
deffunc H2( Element of (T |^ the carrier of S)) ->  Element of the carrier of T = "\/" ( {  ($1 . i4) where i4 is Element of S : i4 in D  }  ,T);
deffunc H3( Element of (T |^ the carrier of S)) ->  set = $1 . (sup D);
A1: P = sup (sF .: D) by Th28;
  {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  is_<=_than P
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in  {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  or b <= P )
assume  b in  {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ; ::_thesis: b <= P
then consider g9 being Element of (T |^ the carrier of S) such that
A2: b = "\/" ( {  (g9 . i) where i is Element of S : i in D  }  ,T) and
A3: g9 in F ;
reconsider g1 = g9 as continuous Function of S,T by A3, Th21;
 g9 <= "\/" (F,(T |^ the carrier of S)) by A3, YELLOW_2:22;
then A4: g1 <= sF by WAYBEL10:11;
A5: g1 .: D is_<=_than sup (sF .: D)
proof
let a be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not a in g1 .: D or a <= sup (sF .: D) )
assume  a in g1 .: D ; ::_thesis: a <= sup (sF .: D)
then consider x being set  such that
A6: x in dom g1 and
A7: x in D and
A8: a = g1 . x by FUNCT_1:def_6;
reconsider x9 = x as Element of S by A6;
 x in the carrier of S by A6;
then  x9 in dom sF by FUNCT_2:def_1;
then  sF . x9 in sF .: D by A7, FUNCT_1:def_6;
then A9: sF . x9 <= sup (sF .: D) by YELLOW_2:22;
 g1 . x9 <= sF . x9 by A4, YELLOW_2:9;
hence  a <= sup (sF .: D) by A8, A9, YELLOW_0:def_2; ::_thesis: verum
end;
 the carrier of S c= dom g1 by FUNCT_2:def_1;
then A10: the carrier of S c= dom g9 ;
 g9 .:  {  H1(i2) where i2 is Element of S : S2[i2]  }  =  {  (g9 . H1(i)) where i is Element of S : S2[i]  }  from WAYBEL24:sch_5(A10);
then  b = "\/" ((g9 .: D),T) by A2, Lm1;
hence  b <= P by A1, A5, YELLOW_0:32; ::_thesis: verum
end;
then A11: L <= P by YELLOW_0:32;
A12: for g8 being Element of (T |^ the carrier of S) st S1[g8] holds
H2(g8) = H3(g8)
proof
let g1 be Element of (T |^ the carrier of S); ::_thesis: ( S1[g1] implies H2(g1) = H3(g1) )
assume  g1 in F ; ::_thesis: H2(g1) = H3(g1)
then reconsider g9 = g1 as continuous Function of S,T by Th21;
A13: ( g9 preserves_sup_of D & ex_sup_of D,S ) by WAYBEL_0:def_37, YELLOW_0:17;
 the carrier of S c= dom g9 by FUNCT_2:def_1;
then A14: the carrier of S c= dom g1 ;
 g1 .:  {  H1(i2) where i2 is Element of S : S2[i2]  }  =  {  (g1 . H1(i)) where i is Element of S : S2[i]  }  from WAYBEL24:sch_5(A14);
then  "\/" ( {  (g1 . i) where i is Element of S : i in D  }  ,T) = sup (g9 .: D) by Lm1
.= g1 . (sup D) by A13, WAYBEL_0:def_31 ;
hence  H2(g1) = H3(g1) ; ::_thesis: verum
end;
  {  H2(g3) where g3 is Element of (T |^ the carrier of S) : S1[g3]  }  =  {  H3(g4) where g4 is Element of (T |^ the carrier of S) : S1[g4]  }  from WAYBEL24:sch_4(A12);
then A15: L = sF . (sup D) by Th26;
  {  ("\/" ( {  (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F  }  ,T)) where i3 is Element of S : i3 in D  }  is_<=_than L
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in  {  ("\/" ( {  (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F  }  ,T)) where i3 is Element of S : i3 in D  }  or b <= L )
assume  b in  {  ("\/" ( {  (g2 . i3) where g2 is Element of (T |^ the carrier of S) : g2 in F  }  ,T)) where i3 is Element of S : i3 in D  }  ; ::_thesis: b <= L
then consider i9 being Element of S such that
A16: b = "\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T) and
A17: i9 in D ;
 i9 in the carrier of S ;
then A18: i9 in dom sF by FUNCT_2:def_1;
 b = sF . i9 by A16, Th26;
then  b in sF .: D by A17, A18, FUNCT_1:def_6;
then A19: b <= sup (sF .: D) by YELLOW_2:22;
 sF is monotone by Th29;
then  sup (sF .: D) <= L by A15, WAYBEL17:15;
hence  b <= L by A19, YELLOW_0:def_2; ::_thesis: verum
end;
then  P <= L by YELLOW_0:32;
hence  "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T) = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T) by A11, YELLOW_0:def_3; ::_thesis: verum
end;

theorem Th31: :: WAYBEL24:31
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
let D be non empty directed Subset of S; ::_thesis: "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)
 ContMaps (S,T) is full SubRelStr of T |^ the carrier of S by Def3;
then  the carrier of (ContMaps (S,T)) c= the carrier of (T |^ the carrier of S) by YELLOW_0:def_13;
then reconsider F9 = F as non empty Subset of (T |^ the carrier of S) by XBOOLE_1:1;
reconsider sF = sup F9 as Function of S,T by Th19;
set L = "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T);
set P = "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T);
deffunc H1( Element of (T |^ the carrier of S)) ->  Element of the carrier of T = "\/" ( {  ($1 . i4) where i4 is Element of S : i4 in D  }  ,T);
deffunc H2( Element of (T |^ the carrier of S)) ->  set = $1 . (sup D);
defpred S1[ set ] means $1 in F9;
A1: for g8 being Element of (T |^ the carrier of S) st S1[g8] holds
H1(g8) = H2(g8)
proof
deffunc H3( Element of S) ->  Element of S = $1;
let g1 be Element of (T |^ the carrier of S); ::_thesis: ( S1[g1] implies H1(g1) = H2(g1) )
assume  g1 in F9 ; ::_thesis: H1(g1) = H2(g1)
then reconsider g9 = g1 as continuous Function of S,T by Th21;
defpred S2[ set ] means $1 in D;
A2: ( g9 preserves_sup_of D & ex_sup_of D,S ) by WAYBEL_0:def_37, YELLOW_0:17;
 the carrier of S c= dom g9 by FUNCT_2:def_1;
then A3: the carrier of S c= dom g1 ;
 g1 .:  {  H3(i2) where i2 is Element of S : S2[i2]  }  =  {  (g1 . H3(i)) where i is Element of S : S2[i]  }  from WAYBEL24:sch_5(A3);
then  "\/" ( {  (g1 . i) where i is Element of S : i in D  }  ,T) = sup (g9 .: D) by Lm1
.= g1 . (sup D) by A2, WAYBEL_0:def_31 ;
hence  H1(g1) = H2(g1) ; ::_thesis: verum
end;
  {  H1(g3) where g3 is Element of (T |^ the carrier of S) : S1[g3]  }  =  {  H2(g4) where g4 is Element of (T |^ the carrier of S) : S1[g4]  }  from WAYBEL24:sch_4(A1);
then A4: "\/" ( {  ("\/" ( {  (g . i) where i is Element of S : i in D  }  ,T)) where g is Element of (T |^ the carrier of S) : g in F  }  ,T) = sF . (sup D) by Th25;
 "\/" ( {  ("\/" ( {  (g9 . i9) where g9 is Element of (T |^ the carrier of S) : g9 in F  }  ,T)) where i9 is Element of S : i9 in D  }  ,T) = sup (sF .: D) by Th27;
hence  "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D) by A4, Th30; ::_thesis: verum
end;

theorem Th32: :: WAYBEL24:32
for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))
proof
let S, T be complete Scott TopLattice; ::_thesis: for F being non empty Subset of (ContMaps (S,T)) holds "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))
let F be non empty Subset of (ContMaps (S,T)); ::_thesis: "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T))
reconsider Ex = "\/" (F,(T |^ the carrier of S)) as Function of S,T by Th19;
 for X being Subset of S st not X is empty & X is directed holds
Ex preserves_sup_of X
proof
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies Ex preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: Ex preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
 Ex preserves_sup_of X9
proof
assume  ex_sup_of X9,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of Ex .: X9,T & "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) )
thus  ex_sup_of Ex .: X9,T by YELLOW_0:17; ::_thesis: "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S))
thus  "\/" ((Ex .: X9),T) = Ex . ("\/" (X9,S)) by Th31; ::_thesis: verum
end;
hence  Ex preserves_sup_of X ; ::_thesis: verum
end;
then  Ex is directed-sups-preserving by WAYBEL_0:def_37;
hence  "\/" (F,(T |^ the carrier of S)) in the carrier of (ContMaps (S,T)) by Def3; ::_thesis: verum
end;

theorem Th33: :: WAYBEL24:33
for S being non empty RelStr
for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty antisymmetric lower-bounded RelStr holds Bottom (T |^ the carrier of S) = S --> (Bottom T)
let T be non empty antisymmetric lower-bounded RelStr ; ::_thesis: Bottom (T |^ the carrier of S) = S --> (Bottom T)
set L = T |^ the carrier of S;
reconsider f = S --> (Bottom T) as Element of (T |^ the carrier of S) by Th19;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (T |^ the carrier of S) st b is_>=_than {} holds
f <= b
proof
let b be Element of (T |^ the carrier of S); ::_thesis: ( b is_>=_than {} implies f <= b )
reconsider b9 = b as Function of S,T by Th19;
assume  b is_>=_than {} ; ::_thesis: f <= b
 for x being Element of S holds f9 . x <= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x <= b9 . x
f9 . x = ( the carrier of S --> (Bottom T)) . x
.= Bottom T by FUNCOP_1:7 ;
hence  f9 . x <= b9 . x by YELLOW_0:44; ::_thesis: verum
end;
then  f9 <= b9 by YELLOW_2:9;
hence  f <= b by WAYBEL10:11; ::_thesis: verum
end;
 f is_>=_than {} by YELLOW_0:6;
then  f = "\/" ({},(T |^ the carrier of S)) by A1, YELLOW_0:30;
hence  Bottom (T |^ the carrier of S) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum
end;

theorem :: WAYBEL24:34
for S being non empty RelStr
for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)
proof
let S be non empty RelStr ; ::_thesis: for T being non empty antisymmetric upper-bounded RelStr holds Top (T |^ the carrier of S) = S --> (Top T)
let T be non empty antisymmetric upper-bounded RelStr ; ::_thesis: Top (T |^ the carrier of S) = S --> (Top T)
set L = T |^ the carrier of S;
reconsider f = S --> (Top T) as Element of (T |^ the carrier of S) by Th19;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (T |^ the carrier of S) st b is_<=_than {} holds
f >= b
proof
let b be Element of (T |^ the carrier of S); ::_thesis: ( b is_<=_than {} implies f >= b )
reconsider b9 = b as Function of S,T by Th19;
assume  b is_<=_than {} ; ::_thesis: f >= b
 for x being Element of S holds f9 . x >= b9 . x
proof
let x be Element of S; ::_thesis: f9 . x >= b9 . x
f9 . x = ( the carrier of S --> (Top T)) . x
.= Top T by FUNCOP_1:7 ;
hence  f9 . x >= b9 . x by YELLOW_0:45; ::_thesis: verum
end;
then  f9 >= b9 by YELLOW_2:9;
hence  f >= b by WAYBEL10:11; ::_thesis: verum
end;
 f is_<=_than {} by YELLOW_0:6;
then  f = "/\" ({},(T |^ the carrier of S)) by A1, YELLOW_0:31;
hence  Top (T |^ the carrier of S) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum
end;

registration
let S be non empty reflexive RelStr ;
let T be complete LATTICE;
let a be Element of T;
clusterS --> a ->  directed-sups-preserving ;
coherence
 S --> a is directed-sups-preserving
proof
set f = S --> a;
 for X being Subset of S st not X is empty & X is directed holds
S --> a preserves_sup_of X
proof
let X be Subset of S; ::_thesis: ( not X is empty & X is directed implies S --> a preserves_sup_of X )
assume  ( not X is empty & X is directed ) ; ::_thesis: S --> a preserves_sup_of X
then reconsider X9 = X as non empty directed Subset of S ;
 S --> a preserves_sup_of X
proof
assume  ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (S --> a) .: X,T & "\/" (((S --> a) .: X),T) = (S --> a) . ("\/" (X,S)) )
thus  ex_sup_of (S --> a) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((S --> a) .: X),T) = (S --> a) . ("\/" (X,S))
A1: {a} c= (S --> a) .: X
proof
set n = the Element of X9;
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in {a} or b in (S --> a) .: X )
A2: a = ( the carrier of S --> a) . the Element of X9 by FUNCOP_1:7
.= (S --> a) . the Element of X9 ;
assume  b in {a} ; ::_thesis: b in (S --> a) .: X
then A3: b = a by TARSKI:def_1;
 dom (S --> a) = the carrier of S by FUNCOP_1:13;
hence  b in (S --> a) .: X by A3, A2, FUNCT_1:def_6; ::_thesis: verum
end;
 (S --> a) .: X c= rng (S --> a) by RELAT_1:111;
then  (S --> a) .: X c= {a} by FUNCOP_1:8;
hence  sup ((S --> a) .: X) = sup {a} by A1, XBOOLE_0:def_10
.= a by YELLOW_0:39
.= ( the carrier of S --> a) . (sup X) by FUNCOP_1:7
.= (S --> a) . (sup X) ;
::_thesis: verum
end;
hence  S --> a preserves_sup_of X ; ::_thesis: verum
end;
hence  S --> a is directed-sups-preserving by WAYBEL_0:def_37; ::_thesis: verum
end;
end;

theorem Th35: :: WAYBEL24:35
for S, T being complete Scott TopLattice holds ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
proof
let S, T be complete Scott TopLattice; ::_thesis: ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S
set L = T |^ the carrier of S;
reconsider CS = ContMaps (S,T) as full SubRelStr of T |^ the carrier of S by Def3;
now__::_thesis:_for_X_being_Subset_of_CS_st_ex_sup_of_X,T_|^_the_carrier_of_S_holds_
"\/"_(X,(T_|^_the_carrier_of_S))_in_the_carrier_of_CS
let X be Subset of CS; ::_thesis: ( ex_sup_of X,T |^ the carrier of S implies "\/" (b1,(T |^ the carrier of S)) in the carrier of CS )
assume  ex_sup_of X,T |^ the carrier of S ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
percases ( not X is empty or X is empty ) ;
suppose not X is empty ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
hence  "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Th32; ::_thesis: verum
end;
suppose X is empty ; ::_thesis: "\/" (b1,(T |^ the carrier of S)) in the carrier of CS
then  "\/" (X,(T |^ the carrier of S)) = Bottom (T |^ the carrier of S) by YELLOW_0:def_11;
then  "\/" (X,(T |^ the carrier of S)) = S --> (Bottom T) by Th33;
hence  "\/" (X,(T |^ the carrier of S)) in the carrier of CS by Def3; ::_thesis: verum
end;
end;
end;
hence  ContMaps (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S by YELLOW_0:def_19; ::_thesis: verum
end;

registration
let S, T be complete Scott TopLattice;
cluster ContMaps (S,T) ->  strict complete ;
coherence
 ContMaps (S,T) is complete
proof
 ContMaps (S,T) is non empty full sups-inheriting SubRelStr of T |^ the carrier of S by Def3, Th35;
hence  ContMaps (S,T) is complete by YELLOW_2:31; ::_thesis: verum
end;
end;

theorem :: WAYBEL24:36
for S, T being non empty complete Scott TopLattice holds Bottom (ContMaps (S,T)) = S --> (Bottom T)
proof
let S, T be non empty complete Scott TopLattice; ::_thesis: Bottom (ContMaps (S,T)) = S --> (Bottom T)
set L = ContMaps (S,T);
reconsider f = S --> (Bottom T) as Element of (ContMaps (S,T)) by Th21;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (ContMaps (S,T)) st b is_>=_than {} holds
f <= b
proof
let b be Element of (ContMaps (S,T)); ::_thesis: ( b is_>=_than {} implies f <= b )
reconsider b9 = b as Function of S,T by Th21;
assume  b is_>=_than {} ; ::_thesis: f <= b
 for i being Element of S holds [(f . i),(b . i)] in the InternalRel of T
proof
let i be Element of S; ::_thesis: [(f . i),(b . i)] in the InternalRel of T
f . i = ( the carrier of S --> (Bottom T)) . i
.= Bottom T by FUNCOP_1:7 ;
then  f9 . i <= b9 . i by YELLOW_0:44;
hence  [(f . i),(b . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
hence  f <= b by Th20; ::_thesis: verum
end;
 f is_>=_than {} by YELLOW_0:6;
then  f = "\/" ({},(ContMaps (S,T))) by A1, YELLOW_0:30;
hence  Bottom (ContMaps (S,T)) = S --> (Bottom T) by YELLOW_0:def_11; ::_thesis: verum
end;

theorem :: WAYBEL24:37
for S, T being non empty complete Scott TopLattice holds Top (ContMaps (S,T)) = S --> (Top T)
proof
let S, T be non empty complete Scott TopLattice; ::_thesis: Top (ContMaps (S,T)) = S --> (Top T)
set L = ContMaps (S,T);
reconsider f = S --> (Top T) as Element of (ContMaps (S,T)) by Th21;
reconsider f9 = f as Function of S,T ;
A1: for b being Element of (ContMaps (S,T)) st b is_<=_than {} holds
f >= b
proof
let b be Element of (ContMaps (S,T)); ::_thesis: ( b is_<=_than {} implies f >= b )
reconsider b9 = b as Function of S,T by Th21;
assume  b is_<=_than {} ; ::_thesis: f >= b
 for i being Element of S holds [(b . i),(f . i)] in the InternalRel of T
proof
let i be Element of S; ::_thesis: [(b . i),(f . i)] in the InternalRel of T
f . i = ( the carrier of S --> (Top T)) . i
.= Top T by FUNCOP_1:7 ;
then  f9 . i >= b9 . i by YELLOW_0:45;
hence  [(b . i),(f . i)] in the InternalRel of T by ORDERS_2:def_5; ::_thesis: verum
end;
hence  f >= b by Th20; ::_thesis: verum
end;
 f is_<=_than {} by YELLOW_0:6;
then  f = "/\" ({},(ContMaps (S,T))) by A1, YELLOW_0:31;
hence  Top (ContMaps (S,T)) = S --> (Top T) by YELLOW_0:def_12; ::_thesis: verum
end;

theorem :: WAYBEL24:38
for S, T being complete Scott TopLattice holds SCMaps (S,T) = ContMaps (S,T)
proof
let S, T be complete Scott TopLattice; ::_thesis: SCMaps (S,T) = ContMaps (S,T)
reconsider Sm = ContMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by Def3;
reconsider SC = SCMaps (S,T) as non empty full SubRelStr of T |^ the carrier of S by WAYBEL15:1;
A1: the carrier of SC c= the carrier of (MonMaps (S,T)) by YELLOW_0:def_13;
A2: the carrier of SC c= the carrier of Sm
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of SC or a in the carrier of Sm )
assume A3: a in the carrier of SC ; ::_thesis: a in the carrier of Sm
then reconsider f = a as Function of S,T by A1, WAYBEL10:9;
 f is continuous Function of S,T by A3, WAYBEL17:def_2;
then  a is Element of Sm by Th21;
hence  a in the carrier of Sm ; ::_thesis: verum
end;
 the carrier of Sm c= the carrier of SC
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in the carrier of Sm or a in the carrier of SC )
assume  a in the carrier of Sm ; ::_thesis: a in the carrier of SC
then  a is continuous Function of S,T by Th21;
hence  a in the carrier of SC by WAYBEL17:def_2; ::_thesis: verum
end;
then  the carrier of SC = the carrier of Sm by A2, XBOOLE_0:def_10;
hence  SCMaps (S,T) = ContMaps (S,T) by YELLOW_0:57; ::_thesis: verum
end;