let X, Y be non empty TopSpace; :: thesis: for S being Scott TopAugmentation of InclPoset the topology of Y

for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds

f is continuous

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds

f is continuous

let f be Function of X,S; :: thesis: ( *graph f is open Subset of [:X,Y:] implies f is continuous )

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: f is continuous

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;

hence f is continuous by A6, TOPS_2:43; :: thesis: verum

for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds

f is continuous

let S be Scott TopAugmentation of InclPoset the topology of Y; :: thesis: for f being Function of X,S st *graph f is open Subset of [:X,Y:] holds

f is continuous

let f be Function of X,S; :: thesis: ( *graph f is open Subset of [:X,Y:] implies f is continuous )

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: f is continuous

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: for P being Subset of S st P is open holds

f " P is open

[#] S <> {}
;f " P is open

let P be Subset of S; :: thesis: ( P is open implies f " P is open )

assume A7: P is open ; :: thesis: f " P is open

end;assume A7: P is open ; :: thesis: f " P is open

now :: thesis: for x being set holds

( ( x in f " P implies ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )

hence
f " P is open
by TOPS_1:25; :: thesis: verum( ( x in f " P implies ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )

let x be set ; :: thesis: ( ( x in f " P implies ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) ) & ( ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )

( Q is open & Q c= f " P & x in Q ) ; :: thesis: x in f " P

hence x in f " P ; :: thesis: verum

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

( Q is open & Q c= f " P & x in Q ) implies x in f " P ) )

hereby :: thesis: ( ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q ) implies x in f " P )

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

defpred S_{1}[ 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: ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q )

then reconsider y = x as Element of X ;

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_{1}[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

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

A25: proj2 (rng g) c= bool (f . x)

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_{2}[ 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;

A50: ( dom hh = A & rng hh c= W ) and

A51: for c being object st c in A holds

S_{2}[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: ( Q is open & Q c= f " P & x in Q )

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: ( Q c= f " P & x in Q )

thus Q c= f " P :: thesis: x in Q

end;assume A8: x in f " P ; :: thesis: ex Q being Subset of X st

( Q is open & Q c= f " P & x in Q )

then reconsider y = x as Element of X ;

A9: now :: thesis: for e being object st e in f . x holds

ex u being object st

( u in [: the topology of X, the topology of Y:] & S_{1}[e,u] )

consider g being Function such that ex u being object st

( u in [: the topology of X, the topology of Y:] & S

let e be object ; :: thesis: ( e in f . x implies ex u being object st

( u in [: the topology of X, the topology of Y:] & S_{1}[e,u] ) )

assume e in f . x ; :: thesis: ex u being object st

( u in [: the topology of X, the topology of Y:] & S_{1}[e,u] )

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: ( u in [: the topology of X, the topology of Y:] & S_{1}[e,u] )

( 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: S_{1}[e,u]

thus S_{1}[e,u]
by A3, A10, A11, A12, ZFMISC_1:74, ZFMISC_1:87; :: thesis: verum

end;( u in [: the topology of X, the topology of Y:] & S

assume e in f . x ; :: thesis: ex u being object st

( u in [: the topology of X, the topology of Y:] & S

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: ( u in [: the topology of X, the topology of Y:] & S

( 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: S

thus S

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

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

{} (proj2 (rng g)) in { (union A) where A is Subset of (proj2 (rng g)) : A is finite }
by ZFMISC_1:2;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } or x in the topology of Y )

assume x in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } ; :: thesis: x in the topology of Y

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: verum

end;assume x in { (union A) where A is Subset of (proj2 (rng g)) : A is finite } ; :: thesis: x in the topology of Y

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: verum

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

then reconsider J9 = J as non empty directed Subset of S by A1, WAYBEL_0:3;
let a, b be Element of (InclPoset the topology of Y); :: according to WAYBEL_0:def 1 :: thesis: ( not a in J or not b in J or ex b_{1} being Element of the carrier of (InclPoset the topology of Y) st

( b_{1} in J & a <= b_{1} & b <= b_{1} ) )

assume a in J ; :: thesis: ( not b in J or ex b_{1} being Element of the carrier of (InclPoset the topology of Y) st

( b_{1} in J & a <= b_{1} & b <= b_{1} ) )

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: ex b_{1} being Element of the carrier of (InclPoset the topology of Y) st

( b_{1} in J & a <= b_{1} & b <= b_{1} )

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: ( ab in J & a <= ab & b <= ab )

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 <= ab & b <= ab )

( a c= ab & b c= ab ) by A24, XBOOLE_1:7;

hence ( a <= ab & b <= ab ) by YELLOW_1:3; :: thesis: verum

end;( b

assume a in J ; :: thesis: ( not b in J or ex b

( b

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: ex b

( b

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: ( ab in J & a <= ab & b <= ab )

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 <= ab & b <= ab )

( a c= ab & b c= ab ) by A24, XBOOLE_1:7;

hence ( a <= ab & b <= ab ) by YELLOW_1:3; :: thesis: verum

A25: proj2 (rng g) c= bool (f . x)

proof

union J = f . y
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in proj2 (rng g) or z in bool (f . x) )

reconsider zz = z as set by TARSKI:1;

assume z in proj2 (rng g) ; :: thesis: z in bool (f . x)

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

end;reconsider zz = z as set by TARSKI:1;

assume z in proj2 (rng g) ; :: thesis: z in bool (f . x)

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

hence
z in bool (f . x)
; :: thesis: verum
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in zz or a in f . x )

assume a in zz ; :: thesis: a in f . x

then [x,a] in [:zz1,zz:] by A29, ZFMISC_1:87;

hence a in f . x by A30, Th38; :: thesis: verum

end;assume a in zz ; :: thesis: a in f . x

then [x,a] in [:zz1,zz:] by A29, ZFMISC_1:87;

hence a in f . x by A30, Th38; :: thesis: verum

proof

then
sup J = f . y
by YELLOW_1:22;
thus
union J c= f . y
:: according to XBOOLE_0:def 10 :: thesis: f . y c= union J

assume A34: a in f . y ; :: thesis: a in union J

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: verum

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in f . y or a in union J )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union J or a in f . y )

assume a in union J ; :: thesis: a in f . y

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: verum

end;assume a in union J ; :: thesis: a in f . y

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: verum

assume A34: a in f . y ; :: thesis: a in union J

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: verum

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

( 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: for c being object st c in A holds

ex a being object st

( a in W & S_{2}[c,a] )

consider hh being Function such that ex a being object st

( a in W & S

let c be object ; :: thesis: ( c in A implies ex a being object st

( a in W & S_{2}[c,a] ) )

assume c in A ; :: thesis: ex a being object st

( a in W & S_{2}[c,a] )

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: ( a in W & S_{2}[c,a] )

thus a in W by A14, A45; :: thesis: S_{2}[c,a]

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_{2}[c,a]
by A14, A15, A45, A46, A49, A48; :: thesis: verum

end;( a in W & S

assume c in A ; :: thesis: ex a being object st

( a in W & S

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: ( a in W & S

thus a in W by A14, A45; :: thesis: S

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

A50: ( dom hh = A & rng hh c= W ) and

A51: for c being object st c in A holds

S

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: ( Q is open & Q c= f " P & x in Q )

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: ( Q c= f " P & x in Q )

thus Q c= f " P :: thesis: x in Q

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Q or z in f " P )

assume A53: z in Q ; :: thesis: z in f " P

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

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: verum

end;assume A53: z in Q ; :: thesis: z in f " P

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

then
aa <= fz
by YELLOW_1:3;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in a or p in f . zz )

assume p in a ; :: thesis: p in f . zz

then consider q being set such that

A54: p in q and

A55: q in A by A41, TARSKI:def 4;

S_{2}[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: verum

end;assume p in a ; :: thesis: p in f . zz

then consider q being set such that

A54: p in q and

A55: q in A by A41, TARSKI:def 4;

S

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: verum

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: verum

now :: thesis: for c1 being set st c1 in B holds

x in c1

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

let c1 be set ; :: thesis: ( c1 in B implies x in c1 )

assume c1 in B ; :: thesis: x in c1

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: verum

end;assume c1 in B ; :: thesis: x in c1

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: verum

( Q is open & Q c= f " P & x in Q ) ; :: thesis: x in f " P

hence x in f " P ; :: thesis: verum

hence f is continuous by A6, TOPS_2:43; :: thesis: verum