let X, Y be non empty TopSpace; :: thesis:
let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis:
let f be Function of X,S; :: thesis:
A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of (InclPoset the topology of Y), the InternalRel of (InclPoset the topology of Y) #) by YELLOW_9:def 4;
A2: dom f = the carrier of X by FUNCT_2:def 1;
assume *graph f is open Subset of [:X,Y:] ; :: thesis:
then consider AA being Subset-Family of [:X,Y:] such that
A3: *graph f = union AA and
A4: for e being set st e in AA holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
A5: the carrier of (InclPoset the topology of Y) = the topology of Y by YELLOW_1:1;

A6: now :: thesis:

let P be Subset of S; :: thesis:
assume A7: P is open ; :: thesis:

now :: thesis:

let x be set ; :: thesis:

hereby :: thesis:

defpred S₁[ object , object ] means ( x in $2 `1 & $1 in $2 `2 & [:($2 `1),($2 `2):] c= *graph f );
assume A8: x in f " P ; :: thesis:
then reconsider y = x as Element of X ;

A9: now :: thesis:

let e be object ; :: thesis:
assume e in f . x ; :: thesis:
then [x,e] in *graph f by A2, A8, Th38;
then consider V being set such that
A10: [x,e] in V and
A11: V in AA by A3, TARSKI:def 4;
consider A being Subset of X, B being Subset of Y such that
A12: V = [:A,B:] and
A13: ( A is open & B is open ) by A4, A11;
reconsider u = [A,B] as object ;
take u = u; :: thesis:
( A in the topology of X & B in the topology of Y ) by A13, PRE_TOPC:def 2;
hence u in [: the topology of X, the topology of Y:] by ZFMISC_1:87; :: thesis:
thus S₁[e,u] by A3, A10, A11, A12, ZFMISC_1:74, ZFMISC_1:87; :: thesis:

end;

consider g being Function such that
A14: ( dom g = f . x & rng g c= [: the topology of X, the topology of Y:] ) and
A15: for a being object st a in f . x holds
S₁[a,g . a] from FUNCT_1:sch 6(A9);
set J = { (union A) where A is Subset of (proj2 (rng g)) : A is finite } ;
A16: proj2 (rng g) c= the topology of Y by A14, FUNCT_5:11;
A17: { (union A) where A is Subset of (proj2 (rng g)) : A is finite } c= the topology of Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } ; :: thesis:
then consider A being Subset of (proj2 (rng g)) such that
A18: x = union A and
A is finite ;
A19: A c= the topology of Y by A16;
then A is Subset-Family of Y by XBOOLE_1:1;
hence x in the topology of Y by A18, A19, PRE_TOPC:def 1; :: thesis:

end;

{} (proj2 (rng g)) in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } by ZFMISC_1:2;
then reconsider J = { (union A) where A is Subset of (proj2 (rng g)) : A is finite } as non empty Subset of (InclPoset the topology of Y) by A17, YELLOW_1:1;
J is directed

proof

let a, b be Element of (InclPoset the topology of Y); :: according to WAYBEL_0:def 1 :: thesis:
assume a in J ; :: thesis:
then consider A being Subset of (proj2 (rng g)) such that
A20: a = union A and
A21: A is finite ;
assume b in J ; :: thesis:
then consider B being Subset of (proj2 (rng g)) such that
A22: b = union B and
A23: B is finite ;
reconsider AB = A \/ B as finite Subset of (proj2 (rng g)) by A21, A23;
take ab = a "\/" b; :: thesis:
A24: a \/ b = ab by WAYBEL14:18;
union AB = a \/ b by A20, A22, ZFMISC_1:78;
hence ab in J by A24; :: thesis:
( a c= ab & b c= ab ) by A24, XBOOLE_1:7;
hence ( a <= ab & b <= ab ) by YELLOW_1:3; :: thesis:

end;

then reconsider J9 = J as non empty directed Subset of S by A1, WAYBEL_0:3;
A25: proj2 (rng g) c= bool (f . x)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
reconsider zz = z as set by TARSKI:1;
assume z in proj2 (rng g) ; :: thesis:
then consider z1 being object such that
A26: [z1,z] in rng g by XTUPLE_0:def 13;
A27: [z1,z] `1 = z1 ;
reconsider zz1 = z1 as set by TARSKI:1;
A28: ex a being object st
( a in dom g & [z1,z] = g . a ) by A26, FUNCT_1:def 3;
then A29: x in zz1 by A14, A15, A27;
[z1,z] `2 = z ;
then A30: [:zz1,zz:] c= *graph f by A14, A15, A28, A27;
zz c= f . x

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in zz ; :: thesis:
then [x,a] in [:zz1,zz:] by A29, ZFMISC_1:87;
hence a in f . x by A30, Th38; :: thesis:

end;

hence z in bool (f . x) ; :: thesis:

end;

union J = f . y

proof

thus union J c= f . y :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union J ; :: thesis:
then consider u being set such that
A31: a in u and
A32: u in J by TARSKI:def 4;
consider A being Subset of (proj2 (rng g)) such that
A33: u = union A and
A is finite by A32;
A c= bool (f . y) by A25;
then u c= union (bool (f . y)) by A33, ZFMISC_1:77;
then u c= f . y by ZFMISC_1:81;
hence a in f . y by A31; :: thesis:

end;

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: a in f . y ; :: thesis:
then A35: g . a in rng g by A14, FUNCT_1:def 3;
then g . a = [((g . a) `1),((g . a) `2)] by A14, MCART_1:21;
then (g . a) `2 in proj2 (rng g) by A35, XTUPLE_0:def 13;
then reconsider A = {((g . a) `2)} as Subset of (proj2 (rng g)) by ZFMISC_1:31;
union A = (g . a) `2 by ZFMISC_1:25;
then A36: (g . a) `2 in J ;
a in (g . a) `2 by A15, A34;
hence a in union J by A36, TARSKI:def 4; :: thesis:

end;

then sup J = f . y by YELLOW_1:22;
then A37: sup J9 = f . y by A1, YELLOW_0:17, YELLOW_0:26;
f . y in the topology of Y by A5, A1;
then reconsider W = f . y as open Subset of Y by PRE_TOPC:def 2;
A38: proj1 (rng g) c= the topology of X by A14, FUNCT_5:11;
defpred S₂[ object , object ] means ex c1, d being set st
( d = $1 & [c1,$1] = g . $2 & x in c1 & $2 in d & $2 in f . x & [:c1,d:] c= *graph f );
f . x in P by A8, FUNCT_2:38;
then J meets P by A7, A37, WAYBEL11:def 1;
then consider a being object such that
A39: a in J and
A40: a in P by XBOOLE_0:3;
reconsider a = a as Element of S by A40;
consider A being Subset of (proj2 (rng g)) such that
A41: a = union A and
A42: A is finite by A39;

A43: now :: thesis:

let c be object ; :: thesis:
assume c in A ; :: thesis:
then consider c1 being object such that
A44: [c1,c] in rng g by XTUPLE_0:def 13;
reconsider cc1 = c1 as set by TARSKI:1;
consider a being object such that
A45: a in dom g and
A46: [c1,c] = g . a by A44, FUNCT_1:def 3;
reconsider cc = c as set by TARSKI:1;
reconsider a = a as object ;
take a = a; :: thesis:
thus a in W by A14, A45; :: thesis:
A47: [c1,c] `1 = c1 ;
then A48: x in cc1 by A14, A15, A45, A46;
A49: [c1,c] `2 = c ;
then [:cc1,cc:] c= *graph f by A14, A15, A45, A46, A47;
hence S₂[c,a] by A14, A15, A45, A46, A49, A48; :: thesis:

end;

consider hh being Function such that
A50: ( dom hh = A & rng hh c= W ) and
A51: for c being object st c in A holds
S₂[c,hh . c] from FUNCT_1:sch 6(A43);
set B = proj1 (g .: (rng hh));
g .: (rng hh) c= rng g by RELAT_1:111;
then proj1 (g .: (rng hh)) c= proj1 (rng g) by XTUPLE_0:8;
then A52: proj1 (g .: (rng hh)) c= the topology of X by A38;
then reconsider B = proj1 (g .: (rng hh)) as Subset-Family of X by XBOOLE_1:1;
reconsider B = B as Subset-Family of X ;
reconsider Q = Intersect B as Subset of X ;
take Q = Q; :: thesis:
g .: (rng hh) is finite by A42, A50, FINSET_1:5, FINSET_1:8;
then B is finite by Th39;
then Q in FinMeetCl the topology of X by A52, CANTOR_1:def 3;
then Q in the topology of X by CANTOR_1:5;
hence Q is open by PRE_TOPC:def 2; :: thesis:
thus Q c= f " P :: thesis:

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A53: z in Q ; :: thesis:
then reconsider zz = z as Element of X ;
reconsider fz = f . zz, aa = a as Element of (InclPoset the topology of Y) by A1;
a c= f . zz

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in a ; :: thesis:
then consider q being set such that
A54: p in q and
A55: q in A by A41, TARSKI:def 4;
S₂[q,hh . q] by A51, A55;
then consider q1, d being set such that
A56: d = q and
A57: [q1,q] = g . (hh . q) and
A58: hh . q in f . x and
A59: [:q1,d:] c= *graph f ;
hh . q in rng hh by A50, A55, FUNCT_1:def 3;
then [q1,q] in g .: (rng hh) by A14, A57, A58, FUNCT_1:def 6;
then q1 in B by XTUPLE_0:def 12;
then zz in q1 by A53, SETFAM_1:43;
then [zz,p] in [:q1,q:] by A54, ZFMISC_1:87;
hence p in f . zz by A59, Th38, A56; :: thesis:

end;

then aa <= fz by YELLOW_1:3;
then a <= f . zz by A1, YELLOW_0:1;
then f . zz in P by A7, A40, WAYBEL_0:def 20;
hence z in f " P by FUNCT_2:38; :: thesis:

end;

now :: thesis:

let c1 be set ; :: thesis:
assume c1 in B ; :: thesis:
then consider c being object such that
A60: [c1,c] in g .: (rng hh) by XTUPLE_0:def 12;
consider b being object such that
b in dom g and
A61: b in rng hh and
A62: [c1,c] = g . b by A60, FUNCT_1:def 6;
consider c9 being object such that
A63: c9 in dom hh and
A64: b = hh . c9 by A61, FUNCT_1:def 3;
ex c91, d being set st
( d = c9 & [c91,c9] = g . (hh . c9) & x in c91 & hh . c9 in d & hh . c9 in f . x & [:c91,d:] c= *graph f ) by A50, A51, A63;
hence x in c1 by A62, A64, XTUPLE_0:1; :: thesis:

end;

hence x in Q by A8, SETFAM_1:43; :: thesis:

end;

assume ex Q being Subset of X st
( Q is open & Q c= f " P & x in Q ) ; :: thesis:
hence x in f " P ; :: thesis:

end;

hence f " P is open by TOPS_1:25; :: thesis:

end;

[#] S <> {} ;
hence f is continuous by A6, TOPS_2:43; :: thesis: