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 H₁( 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 H₂( Element of (T |^ the carrier of S)) -> set = $1 . (sup D);
defpred S₁[ set ] means $1 in F9;
A1: for g8 being Element of (T |^ the carrier of S) st S₁[g8] holds
H₁(g8) = H₂(g8)

proof

deffunc H₃( Element of S) -> Element of S = $1;
let g1 be Element of (T |^ the carrier of S); :: thesis: ( S₁[g1] implies H₁(g1) = H₂(g1) )
assume g1 in F9 ; :: thesis: H₁(g1) = H₂(g1)
then reconsider g9 = g1 as continuous Function of S,T by Th21;
defpred S₂[ 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 .: { H₃(i2) where i2 is Element of S : S₂[i2] } = { (g1 . H₃(i)) where i is Element of S : S₂[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 ;
hence H₁(g1) = H₂(g1) ; :: thesis: verum

end;

{ H₁(g3) where g3 is Element of (T |^ the carrier of S) : S₁[g3] } = { H₂(g4) where g4 is Element of (T |^ the carrier of S) : S₁[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