theorem Th26: :: WAYBEL24:26

for S, T being complete TopLattice
for F being non empty Subset of (ContMaps (S,T))
for i being Element of S holds ("\/" (F,(T |^ the carrier of S))) . i = "\/" ( { (f . i) where f is Element of (T |^ the carrier of S) : f in F } ,T)