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 S₁[ set ] means $1 in F;
deffunc H₁( Element of S) -> Element of S = $1;
defpred S₂[ set ] means $1 in D;
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);
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 object 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 .: { H₁(i2) where i2 is Element of S : S₂[i2] } = { (g9 . H₁(i)) where i is Element of S : S₂[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 S₁[g8] holds
H₂(g8) = H₃(g8)

proof

let g1 be Element of (T |^ the carrier of S); :: thesis: ( S₁[g1] implies H₂(g1) = H₃(g1) )
assume g1 in F ; :: thesis: H₂(g1) = H₃(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 .: { 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(A14);
then "\/" ( { (g1 . i) where i is Element of S : i in D } ,T) = sup (g9 .: D) by Lm1
.= g1 . (sup D) by A13 ;
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(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