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 object ; :: 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 object 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 object ; :: 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;