let X be non empty TopSpace; :: thesis: for L being non empty up-complete Scott TopPoset
for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L

let L be non empty up-complete Scott TopPoset; :: thesis: for F being non empty directed Subset of (ContMaps (X,L)) holds "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L
let F be non empty directed Subset of (ContMaps (X,L)); :: thesis: "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L
set sF = "\/" (F,(L |^ the carrier of X));
Funcs ( the carrier of X, the carrier of L) = the carrier of (L |^ the carrier of X) by YELLOW_1:28;
then reconsider sF = "\/" (F,(L |^ the carrier of X)) as Function of X,L by FUNCT_2:66;
ContMaps (X,L) is full SubRelStr of L |^ the carrier of X by WAYBEL24:def 3;
then reconsider aF = F as non empty directed Subset of (L |^ the carrier of X) by YELLOW_2:7;
A1: now :: thesis: for A being Subset of L st A is open holds
sF " A is open
let A be Subset of L; :: thesis: ( A is open implies sF " A is open )
assume A2: A is open ; :: thesis: sF " A is open
now :: thesis: for x being set holds
( ( x in sF " A implies ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) )
let x be set ; :: thesis: ( ( x in sF " A implies ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q ) ) & ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) )

hereby :: thesis: ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A )
assume A3: x in sF " A ; :: thesis: ex Q being Element of bool the carrier of X st
( Q is open & Q c= sF " A & x in Q )

then A4: sF . x in A by FUNCT_1:def 7;
reconsider y = x as Element of X by A3;
A5: the carrier of X -POS_prod ( the carrier of X => L) = L |^ the carrier of X by YELLOW_1:def 5;
A6: ( the carrier of X => L) . y = L ;
then A7: ( pi (aF,y) is directed & not pi (aF,y) is empty ) by ;
A8: ex_sup_of aF,L |^ the carrier of X by WAYBEL_0:75;
then (sup aF) . y = sup (pi (aF,y)) by ;
then pi (aF,y) meets A by ;
then consider a being object such that
A9: a in pi (aF,y) and
A10: a in A by XBOOLE_0:3;
consider f being Function such that
A11: f in aF and
A12: a = f . y by ;
reconsider f = f as continuous Function of X,L by ;
take Q = f " A; :: thesis: ( Q is open & Q c= sF " A & x in Q )
[#] L <> {} ;
hence Q is open by ; :: thesis: ( Q c= sF " A & x in Q )
A13: dom sF = the carrier of X by FUNCT_2:def 1;
thus Q c= sF " A :: thesis: x in Q
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Q or b in sF " A )
assume A14: b in Q ; :: thesis: b in sF " A
then A15: f . b in A by FUNCT_1:def 7;
reconsider b = b as Element of X by A14;
A16: ( the carrier of X => L) . b = L ;
then ( pi (aF,b) is directed & not pi (aF,b) is empty ) by ;
then A17: ex_sup_of pi (aF,b),L by WAYBEL_0:75;
sF . b = sup (pi (aF,b)) by ;
then A18: sF . b is_>=_than pi (aF,b) by ;
f . b in pi (aF,b) by ;
then f . b <= sF . b by A18;
then sF . b in A by ;
hence b in sF " A by ; :: thesis: verum
end;
dom f = the carrier of X by FUNCT_2:def 1;
hence x in Q by ; :: thesis: verum
end;
thus ( ex Q being Subset of X st
( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) ; :: thesis: verum
end;
hence sF " A is open by TOPS_1:25; :: thesis: verum
end;
[#] L <> {} ;
hence "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L by ; :: thesis: verum