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;

hence "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L by A1, TOPS_2:43; :: thesis: verum

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

[#] L <> {}
;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

end;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 ) )

hence
sF " A is open
by TOPS_1:25; :: thesis: verum( ( 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 ) )

( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) ; :: thesis: verum

end;( 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 )

thus
( 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 A5, YELLOW16:35;

A8: ex_sup_of aF,L |^ the carrier of X by WAYBEL_0:75;

then (sup aF) . y = sup (pi (aF,y)) by A6, A5, YELLOW16:33;

then pi (aF,y) meets A by A2, A4, A7, WAYBEL11:def 1;

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 A9, CARD_3:def 6;

reconsider f = f as continuous Function of X,L by A11, WAYBEL24:21;

take Q = f " A; :: thesis: ( Q is open & Q c= sF " A & x in Q )

[#] L <> {} ;

hence Q is open by A2, TOPS_2:43; :: 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

hence x in Q by A10, A12, FUNCT_1:def 7; :: thesis: verum

end;( 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 A5, YELLOW16:35;

A8: ex_sup_of aF,L |^ the carrier of X by WAYBEL_0:75;

then (sup aF) . y = sup (pi (aF,y)) by A6, A5, YELLOW16:33;

then pi (aF,y) meets A by A2, A4, A7, WAYBEL11:def 1;

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 A9, CARD_3:def 6;

reconsider f = f as continuous Function of X,L by A11, WAYBEL24:21;

take Q = f " A; :: thesis: ( Q is open & Q c= sF " A & x in Q )

[#] L <> {} ;

hence Q is open by A2, TOPS_2:43; :: 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

dom f = the carrier of X
by FUNCT_2:def 1;
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 A5, YELLOW16:35;

then A17: ex_sup_of pi (aF,b),L by WAYBEL_0:75;

sF . b = sup (pi (aF,b)) by A8, A5, A16, YELLOW16:33;

then A18: sF . b is_>=_than pi (aF,b) by A17, YELLOW_0:30;

f . b in pi (aF,b) by A11, CARD_3:def 6;

then f . b <= sF . b by A18;

then sF . b in A by A2, A15, WAYBEL_0:def 20;

hence b in sF " A by A13, FUNCT_1:def 7; :: thesis: verum

end;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 A5, YELLOW16:35;

then A17: ex_sup_of pi (aF,b),L by WAYBEL_0:75;

sF . b = sup (pi (aF,b)) by A8, A5, A16, YELLOW16:33;

then A18: sF . b is_>=_than pi (aF,b) by A17, YELLOW_0:30;

f . b in pi (aF,b) by A11, CARD_3:def 6;

then f . b <= sF . b by A18;

then sF . b in A by A2, A15, WAYBEL_0:def 20;

hence b in sF " A by A13, FUNCT_1:def 7; :: thesis: verum

hence x in Q by A10, A12, FUNCT_1:def 7; :: thesis: verum

( Q is open & Q c= sF " A & x in Q ) implies x in sF " A ) ; :: thesis: verum

hence "\/" (F,(L |^ the carrier of X)) is continuous Function of X,L by A1, TOPS_2:43; :: thesis: verum