theorem Th31: :: WAYBEL24:31

for S, T being complete Scott TopLattice
for F being non empty Subset of (ContMaps (S,T))
for D being non empty directed Subset of S holds "\/" ((("\/" (F,(T |^ the carrier of S))) .: D),T) = ("\/" (F,(T |^ the carrier of S))) . (sup D)