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
A1: ( x in dom ("\/" F,(T |^ the carrier of S)) & x in D & a = ("\/" F,(T |^ the carrier of S)) . x ) by FUNCT_1:def 12;
reconsider x' = x as Element of S by A1;
a = "\/" { (f . x') where f is Element of (T |^ the carrier of S) : f in F } ,T by A1, 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

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
A2: ( a = "\/" { (f . i1) where f is Element of (T |^ the carrier of S) : f in F } ,T & i1 in D ) ;
A3: a = ("\/" F,(T |^ the carrier of S)) . i1 by A2, Th26;
"\/" F,(T |^ the carrier of S) is Function of S,T by Th19;
then dom ("\/" F,(T |^ the carrier of S)) = the carrier of S by FUNCT_2:def 1;
hence a in ("\/" F,(T |^ the carrier of S)) .: D by A2, A3, FUNCT_1:def 12; :: thesis: verum

end;