theorem Th28: :: WAYBEL24:28

for S, T being complete Scott TopLattice
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 }