let S, T be 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)
let F be 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 D be non empty directed Subset of S; "\/" ( { ("\/" ( { (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;
LATTICE3:def 9 ( 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 }
;
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)
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;
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)
{ 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
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; verum