let r be positive real number ; :: thesis:
let o be Point of (TOP-REAL 2); :: thesis:
set D2 = Tdisk o,r;
set S1 = Tcircle o,r;
set OK = (DiffElems (TOP-REAL 2),(TOP-REAL 2)) /\ the carrier of [:(Tdisk o,r),(Tdisk o,r):];
consider s being Point of (Tcircle o,r);
A1: s in the carrier of (Tcircle o,r) ;
A2: the carrier of (Tcircle o,r) = Sphere o,r by TOPREALB:9;
A3: the carrier of (Tdisk o,r) = cl_Ball o,r by Th3;
Sphere o,r c= cl_Ball o,r by TOPREAL9:17;
then A4: s is Point of (Tdisk o,r) by A1, A2, Th3;
A5: s is Point of (TOP-REAL 2) by PRE_TOPC:55;
A6: |.(o - o).| = |.(0. (TOP-REAL 2)).| by EUCLID:46
.= 0 by TOPRNS_1:24 ;
then o is Point of (Tdisk o,r) by A3, TOPREAL9:8;
then [o,s] in [:the carrier of (Tdisk o,r),the carrier of (Tdisk o,r):] by A4, ZFMISC_1:106;
then A7: [o,s] in the carrier of [:(Tdisk o,r),(Tdisk o,r):] by BORSUK_1:def 5;

now

assume A8: o = s ; :: thesis:
A9: Ball o,r misses Sphere o,r by TOPREAL9:19;
o in Ball o,r by A6, TOPREAL9:7;
hence contradiction by A2, A8, A9, XBOOLE_0:3; :: thesis:

end;

then [o,s] in DiffElems (TOP-REAL 2),(TOP-REAL 2) by A5;
then reconsider OK = (DiffElems (TOP-REAL 2),(TOP-REAL 2)) /\ the carrier of [:(Tdisk o,r),(Tdisk o,r):] as non empty Subset of [:(TOP-REAL 2),(TOP-REAL 2):] by A7, XBOOLE_0:def 4;
set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | OK;
let f be continuous Function of (Tdisk o,r),(Tdisk o,r); :: thesis:
assume A10: f has_no_fixpoint ; :: thesis:
set g = BR-map f;
defpred S₁[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x2 `1 ) - (o `1 ) );
A11: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S₁[x,r]

proof

let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
consider x1, x2 being Point of (TOP-REAL 2) such that
A12: x = [x1,x2] by BORSUK_1:50;
take (x2 `1 ) - (o `1 ) ; :: thesis:
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & (x2 `1 ) - (o `1 ) = (x2 `1 ) - (o `1 ) ) by A12; :: thesis:

end;

consider xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A13: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S₁[x,xo . x] from FUNCT_2:sch 3(A11);
defpred S₂[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x2 `2 ) - (o `2 ) );
A14: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S₂[x,r]

proof

let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
consider x1, x2 being Point of (TOP-REAL 2) such that
A15: x = [x1,x2] by BORSUK_1:50;
take (x2 `2 ) - (o `2 ) ; :: thesis:
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & (x2 `2 ) - (o `2 ) = (x2 `2 ) - (o `2 ) ) by A15; :: thesis:

end;

consider yo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A16: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S₂[x,yo . x] from FUNCT_2:sch 3(A14);
defpred S₃[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x1 `1 ) - (x2 `1 ) );
A17: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S₃[x,r]

proof

let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
consider x1, x2 being Point of (TOP-REAL 2) such that
A18: x = [x1,x2] by BORSUK_1:50;
take (x1 `1 ) - (x2 `1 ) ; :: thesis:
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & (x1 `1 ) - (x2 `1 ) = (x1 `1 ) - (x2 `1 ) ) by A18; :: thesis:

end;

consider dx being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A19: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S₃[x,dx . x] from FUNCT_2:sch 3(A17);
defpred S₄[ set , set ] means ex y1, y2 being Point of (TOP-REAL 2) st
( $1 = [y1,y2] & $2 = (y1 `2 ) - (y2 `2 ) );
A20: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S₄[x,r]

proof

let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
consider x1, x2 being Point of (TOP-REAL 2) such that
A21: x = [x1,x2] by BORSUK_1:50;
take (x1 `2 ) - (x2 `2 ) ; :: thesis:
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & (x1 `2 ) - (x2 `2 ) = (x1 `2 ) - (x2 `2 ) ) by A21; :: thesis:

end;

consider dy being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A22: for y being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S₄[y,dy . y] from FUNCT_2:sch 3(A20);
defpred S₅[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = x2 `1 );
A23: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S₅[x,r]

proof

let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
consider x1, x2 being Point of (TOP-REAL 2) such that
A24: x = [x1,x2] by BORSUK_1:50;
take x2 `1 ; :: thesis:
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & x2 `1 = x2 `1 ) by A24; :: thesis:

end;

consider fx2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A25: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S₅[x,fx2 . x] from FUNCT_2:sch 3(A23);
defpred S₆[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = x2 `2 );
A26: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S₆[x,r]

proof

let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
consider x1, x2 being Point of (TOP-REAL 2) such that
A27: x = [x1,x2] by BORSUK_1:50;
take x2 `2 ; :: thesis:
take x1 ; :: thesis:
take x2 ; :: thesis:
thus ( x = [x1,x2] & x2 `2 = x2 `2 ) by A27; :: thesis:

end;

consider fy2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A28: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S₆[x,fy2 . x] from FUNCT_2:sch 3(A26);
reconsider Dx = dx, Dy = dy, fX2 = fx2, fY2 = fy2, Xo = xo, Yo = yo as Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:24;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Xo . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Xo .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
let V be Subset of R^1 ; :: thesis:
assume that
A29: Xo . p in V and
A30: V is open ; :: thesis:
consider p1, p2 being Point of (TOP-REAL 2) such that
A31: p = [p1,p2] and
A32: Xo . p = (p2 `1 ) - (o `1 ) by A13;
set r = (p2 `1 ) - (o `1 );
reconsider V1 = V as open Subset of REAL by A30, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A33: 0 < g and
A34: ].(((p2 `1 ) - (o `1 )) - g),(((p2 `1 ) - (o `1 )) + g).[ c= V1 by A29, A32, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } ; :: thesis:
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `1 ) - g < x & x < (p2 `1 ) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis:

end;

then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W2:] ; :: thesis:
A35: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( (p2 `1 ) - g < (p2 `1 ) - 0 & (p2 `1 ) + 0 < (p2 `1 ) + g ) by A33, XREAL_1:8, XREAL_1:17;
then p2 in W2 by A35;
hence p in [:([#] (TOP-REAL 2)),W2:] by A31, ZFMISC_1:def 2; :: thesis:
W2 is open by PSCOMP_1:66;
hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:46; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in Xo .: [:([#] (TOP-REAL 2)),W2:] ; :: thesis:
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A36: a in [:([#] (TOP-REAL 2)),W2:] and
A37: Xo . a = b by FUNCT_2:116;
consider a1, a2 being Point of (TOP-REAL 2) such that
A38: a = [a1,a2] and
A39: xo . a = (a2 `1 ) - (o `1 ) by A13;
a2 in W2 by A36, A38, ZFMISC_1:106;
then consider x2, y2 being Element of REAL such that
A40: a2 = |[x2,y2]| and
A41: ( (p2 `1 ) - g < x2 & x2 < (p2 `1 ) + g ) ;
a2 `1 = x2 by A40, EUCLID:56;
then ( ((p2 `1 ) - g) - (o `1 ) < (a2 `1 ) - (o `1 ) & (a2 `1 ) - (o `1 ) < ((p2 `1 ) + g) - (o `1 ) ) by A41, XREAL_1:11;
then (a2 `1 ) - (o `1 ) in ].(((p2 `1 ) - (o `1 )) - g),(((p2 `1 ) - (o `1 )) + g).[ by XXREAL_1:4;
hence b in V by A34, A37, A39; :: thesis:

end;

then Xo is continuous by JGRAPH_2:20;
then reconsider xo = xo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by TOPREAL6:83;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Yo . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Yo .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
let V be Subset of R^1 ; :: thesis:
assume that
A42: Yo . p in V and
A43: V is open ; :: thesis:
consider p1, p2 being Point of (TOP-REAL 2) such that
A44: p = [p1,p2] and
A45: Yo . p = (p2 `2 ) - (o `2 ) by A16;
set r = (p2 `2 ) - (o `2 );
reconsider V1 = V as open Subset of REAL by A43, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A46: 0 < g and
A47: ].(((p2 `2 ) - (o `2 )) - g),(((p2 `2 ) - (o `2 )) + g).[ c= V1 by A42, A45, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } ; :: thesis:
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `2 ) - g < y & y < (p2 `2 ) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis:

end;

then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W2:] ; :: thesis:
A48: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( (p2 `2 ) - g < (p2 `2 ) - 0 & (p2 `2 ) + 0 < (p2 `2 ) + g ) by A46, XREAL_1:8, XREAL_1:17;
then p2 in W2 by A48;
hence p in [:([#] (TOP-REAL 2)),W2:] by A44, ZFMISC_1:def 2; :: thesis:
W2 is open by PSCOMP_1:68;
hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:46; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in Yo .: [:([#] (TOP-REAL 2)),W2:] ; :: thesis:
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A49: a in [:([#] (TOP-REAL 2)),W2:] and
A50: Yo . a = b by FUNCT_2:116;
consider a1, a2 being Point of (TOP-REAL 2) such that
A51: a = [a1,a2] and
A52: yo . a = (a2 `2 ) - (o `2 ) by A16;
a2 in W2 by A49, A51, ZFMISC_1:106;
then consider x2, y2 being Element of REAL such that
A53: a2 = |[x2,y2]| and
A54: ( (p2 `2 ) - g < y2 & y2 < (p2 `2 ) + g ) ;
a2 `2 = y2 by A53, EUCLID:56;
then ( ((p2 `2 ) - g) - (o `2 ) < (a2 `2 ) - (o `2 ) & (a2 `2 ) - (o `2 ) < ((p2 `2 ) + g) - (o `2 ) ) by A54, XREAL_1:11;
then (a2 `2 ) - (o `2 ) in ].(((p2 `2 ) - (o `2 )) - g),(((p2 `2 ) - (o `2 )) + g).[ by XXREAL_1:4;
hence b in V by A47, A50, A52; :: thesis:

end;

then Yo is continuous by JGRAPH_2:20;
then reconsider yo = yo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by TOPREAL6:83;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Dx . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
let V be Subset of R^1 ; :: thesis:
assume that
A55: Dx . p in V and
A56: V is open ; :: thesis:
consider p1, p2 being Point of (TOP-REAL 2) such that
A57: p = [p1,p2] and
A58: dx . p = (p1 `1 ) - (p2 `1 ) by A19;
set r = (p1 `1 ) - (p2 `1 );
reconsider V1 = V as open Subset of REAL by A56, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A59: 0 < g and
A60: ].(((p1 `1 ) - (p2 `1 )) - g),(((p1 `1 ) - (p2 `1 )) + g).[ c= V1 by A55, A58, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `1 ) - (g / 2) < x & x < (p1 `1 ) + (g / 2) ) } ;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - (g / 2) < x & x < (p2 `1 ) + (g / 2) ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p1 `1 ) - (g / 2) < x & x < (p1 `1 ) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { |[x,y]| where x, y is Element of REAL : ( (p1 `1 ) - (g / 2) < x & x < (p1 `1 ) + (g / 2) ) } ; :: thesis:
then ex x, y being Element of REAL st
( a = |[x,y]| & (p1 `1 ) - (g / 2) < x & x < (p1 `1 ) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis:

end;

then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `1 ) - (g / 2) < x & x < (p1 `1 ) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - (g / 2) < x & x < (p2 `1 ) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - (g / 2) < x & x < (p2 `1 ) + (g / 2) ) } ; :: thesis:
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `1 ) - (g / 2) < x & x < (p2 `1 ) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis:

end;

then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - (g / 2) < x & x < (p2 `1 ) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
take [:W1,W2:] ; :: thesis:
A61: p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
A62: 0 / 2 < g / 2 by A59, XREAL_1:76;
then ( (p1 `1 ) - (g / 2) < (p1 `1 ) - 0 & (p1 `1 ) + 0 < (p1 `1 ) + (g / 2) ) by XREAL_1:8, XREAL_1:17;
then A63: p1 in W1 by A61;
A64: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( (p2 `1 ) - (g / 2) < (p2 `1 ) - 0 & (p2 `1 ) + 0 < (p2 `1 ) + (g / 2) ) by A62, XREAL_1:8, XREAL_1:17;
then p2 in W2 by A64;
hence p in [:W1,W2:] by A57, A63, ZFMISC_1:def 2; :: thesis:
( W1 is open & W2 is open ) by PSCOMP_1:66;
hence [:W1,W2:] is open by BORSUK_1:46; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in Dx .: [:W1,W2:] ; :: thesis:
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A65: a in [:W1,W2:] and
A66: Dx . a = b by FUNCT_2:116;
consider a1, a2 being Point of (TOP-REAL 2) such that
A67: a = [a1,a2] and
A68: dx . a = (a1 `1 ) - (a2 `1 ) by A19;
a1 in W1 by A65, A67, ZFMISC_1:106;
then consider x1, y1 being Element of REAL such that
A69: a1 = |[x1,y1]| and
A70: (p1 `1 ) - (g / 2) < x1 and
A71: x1 < (p1 `1 ) + (g / 2) ;
A72: a1 `1 = x1 by A69, EUCLID:56;
( ((p1 `1 ) - (g / 2)) + (g / 2) < x1 + (g / 2) & (p1 `1 ) - x1 > (p1 `1 ) - ((p1 `1 ) + (g / 2)) ) by A70, A71, XREAL_1:8, XREAL_1:17;
then ( (p1 `1 ) - x1 < (x1 + (g / 2)) - x1 & (p1 `1 ) - x1 > - (g / 2) ) by XREAL_1:11;
then A73: abs ((p1 `1 ) - x1) < g / 2 by SEQ_2:9;
a2 in W2 by A65, A67, ZFMISC_1:106;
then consider x2, y2 being Element of REAL such that
A74: a2 = |[x2,y2]| and
A75: (p2 `1 ) - (g / 2) < x2 and
A76: x2 < (p2 `1 ) + (g / 2) ;
A77: a2 `1 = x2 by A74, EUCLID:56;
( ((p2 `1 ) - (g / 2)) + (g / 2) < x2 + (g / 2) & (p2 `1 ) - x2 > (p2 `1 ) - ((p2 `1 ) + (g / 2)) ) by A75, A76, XREAL_1:8, XREAL_1:17;
then ( (p2 `1 ) - x2 < (x2 + (g / 2)) - x2 & (p2 `1 ) - x2 > - (g / 2) ) by XREAL_1:11;
then abs ((p2 `1 ) - x2) < g / 2 by SEQ_2:9;
then A78: (abs ((p1 `1 ) - x1)) + (abs ((p2 `1 ) - x2)) < (g / 2) + (g / 2) by A73, XREAL_1:10;
abs (((p1 `1 ) - x1) - ((p2 `1 ) - x2)) <= (abs ((p1 `1 ) - x1)) + (abs ((p2 `1 ) - x2)) by COMPLEX1:143;
then abs (- (((p1 `1 ) - x1) - ((p2 `1 ) - x2))) <= (abs ((p1 `1 ) - x1)) + (abs ((p2 `1 ) - x2)) by COMPLEX1:138;
then abs ((x1 - x2) - ((p1 `1 ) - (p2 `1 ))) < g by A78, XXREAL_0:2;
then (a1 `1 ) - (a2 `1 ) in ].(((p1 `1 ) - (p2 `1 )) - g),(((p1 `1 ) - (p2 `1 )) + g).[ by A72, A77, RCOMP_1:8;
hence b in V by A60, A66, A68; :: thesis:

end;

then Dx is continuous by JGRAPH_2:20;
then reconsider dx = dx as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by TOPREAL6:83;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Dy . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dy .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
let V be Subset of R^1 ; :: thesis:
assume that
A79: Dy . p in V and
A80: V is open ; :: thesis:
consider p1, p2 being Point of (TOP-REAL 2) such that
A81: p = [p1,p2] and
A82: dy . p = (p1 `2 ) - (p2 `2 ) by A22;
set r = (p1 `2 ) - (p2 `2 );
reconsider V1 = V as open Subset of REAL by A80, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A83: 0 < g and
A84: ].(((p1 `2 ) - (p2 `2 )) - g),(((p1 `2 ) - (p2 `2 )) + g).[ c= V1 by A79, A82, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `2 ) - (g / 2) < y & y < (p1 `2 ) + (g / 2) ) } ;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - (g / 2) < y & y < (p2 `2 ) + (g / 2) ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p1 `2 ) - (g / 2) < y & y < (p1 `2 ) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { |[x,y]| where x, y is Element of REAL : ( (p1 `2 ) - (g / 2) < y & y < (p1 `2 ) + (g / 2) ) } ; :: thesis:
then ex x, y being Element of REAL st
( a = |[x,y]| & (p1 `2 ) - (g / 2) < y & y < (p1 `2 ) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis:

end;

then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `2 ) - (g / 2) < y & y < (p1 `2 ) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - (g / 2) < y & y < (p2 `2 ) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - (g / 2) < y & y < (p2 `2 ) + (g / 2) ) } ; :: thesis:
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `2 ) - (g / 2) < y & y < (p2 `2 ) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; :: thesis:

end;

then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - (g / 2) < y & y < (p2 `2 ) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
take [:W1,W2:] ; :: thesis:
A85: p1 = |[(p1 `1 ),(p1 `2 )]| by EUCLID:57;
A86: 0 / 2 < g / 2 by A83, XREAL_1:76;
then ( (p1 `2 ) - (g / 2) < (p1 `2 ) - 0 & (p1 `2 ) + 0 < (p1 `2 ) + (g / 2) ) by XREAL_1:8, XREAL_1:17;
then A87: p1 in W1 by A85;
A88: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( (p2 `2 ) - (g / 2) < (p2 `2 ) - 0 & (p2 `2 ) + 0 < (p2 `2 ) + (g / 2) ) by A86, XREAL_1:8, XREAL_1:17;
then p2 in W2 by A88;
hence p in [:W1,W2:] by A81, A87, ZFMISC_1:def 2; :: thesis:
( W1 is open & W2 is open ) by PSCOMP_1:68;
hence [:W1,W2:] is open by BORSUK_1:46; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in Dy .: [:W1,W2:] ; :: thesis:
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A89: a in [:W1,W2:] and
A90: Dy . a = b by FUNCT_2:116;
consider a1, a2 being Point of (TOP-REAL 2) such that
A91: a = [a1,a2] and
A92: dy . a = (a1 `2 ) - (a2 `2 ) by A22;
a1 in W1 by A89, A91, ZFMISC_1:106;
then consider x1, y1 being Element of REAL such that
A93: a1 = |[x1,y1]| and
A94: (p1 `2 ) - (g / 2) < y1 and
A95: y1 < (p1 `2 ) + (g / 2) ;
A96: a1 `2 = y1 by A93, EUCLID:56;
( ((p1 `2 ) - (g / 2)) + (g / 2) < y1 + (g / 2) & (p1 `2 ) - y1 > (p1 `2 ) - ((p1 `2 ) + (g / 2)) ) by A94, A95, XREAL_1:8, XREAL_1:17;
then ( (p1 `2 ) - y1 < (y1 + (g / 2)) - y1 & (p1 `2 ) - y1 > - (g / 2) ) by XREAL_1:11;
then A97: abs ((p1 `2 ) - y1) < g / 2 by SEQ_2:9;
a2 in W2 by A89, A91, ZFMISC_1:106;
then consider x2, y2 being Element of REAL such that
A98: a2 = |[x2,y2]| and
A99: (p2 `2 ) - (g / 2) < y2 and
A100: y2 < (p2 `2 ) + (g / 2) ;
A101: a2 `2 = y2 by A98, EUCLID:56;
( ((p2 `2 ) - (g / 2)) + (g / 2) < y2 + (g / 2) & (p2 `2 ) - y2 > (p2 `2 ) - ((p2 `2 ) + (g / 2)) ) by A99, A100, XREAL_1:8, XREAL_1:17;
then ( (p2 `2 ) - y2 < (y2 + (g / 2)) - y2 & (p2 `2 ) - y2 > - (g / 2) ) by XREAL_1:11;
then abs ((p2 `2 ) - y2) < g / 2 by SEQ_2:9;
then A102: (abs ((p1 `2 ) - y1)) + (abs ((p2 `2 ) - y2)) < (g / 2) + (g / 2) by A97, XREAL_1:10;
abs (((p1 `2 ) - y1) - ((p2 `2 ) - y2)) <= (abs ((p1 `2 ) - y1)) + (abs ((p2 `2 ) - y2)) by COMPLEX1:143;
then abs (- (((p1 `2 ) - y1) - ((p2 `2 ) - y2))) <= (abs ((p1 `2 ) - y1)) + (abs ((p2 `2 ) - y2)) by COMPLEX1:138;
then abs ((y1 - y2) - ((p1 `2 ) - (p2 `2 ))) < g by A102, XXREAL_0:2;
then (a1 `2 ) - (a2 `2 ) in ].(((p1 `2 ) - (p2 `2 )) - g),(((p1 `2 ) - (p2 `2 )) + g).[ by A96, A101, RCOMP_1:8;
hence b in V by A84, A90, A92; :: thesis:

end;

then Dy is continuous by JGRAPH_2:20;
then reconsider dy = dy as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by TOPREAL6:83;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st fX2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fX2 .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
let V be Subset of R^1 ; :: thesis:
assume that
A103: fX2 . p in V and
A104: V is open ; :: thesis:
consider p1, p2 being Point of (TOP-REAL 2) such that
A105: p = [p1,p2] and
A106: fX2 . p = p2 `1 by A25;
reconsider V1 = V as open Subset of REAL by A104, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A107: 0 < g and
A108: ].((p2 `1 ) - g),((p2 `1 ) + g).[ c= V1 by A103, A106, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } c= the carrier of (TOP-REAL 2)

proof

end;

then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1 ) - g < x & x < (p2 `1 ) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W1:] ; :: thesis:
A109: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( (p2 `1 ) - g < (p2 `1 ) - 0 & (p2 `1 ) + 0 < (p2 `1 ) + g ) by A107, XREAL_1:8, XREAL_1:17;
then p2 in W1 by A109;
hence p in [:([#] (TOP-REAL 2)),W1:] by A105, ZFMISC_1:def 2; :: thesis:
W1 is open by PSCOMP_1:66;
hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:46; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in fX2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis:
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A110: a in [:([#] (TOP-REAL 2)),W1:] and
A111: fX2 . a = b by FUNCT_2:116;
consider a1, a2 being Point of (TOP-REAL 2) such that
A112: a = [a1,a2] and
A113: fX2 . a = a2 `1 by A25;
a2 in W1 by A110, A112, ZFMISC_1:106;
then consider x1, y1 being Element of REAL such that
A114: a2 = |[x1,y1]| and
A115: (p2 `1 ) - g < x1 and
A116: x1 < (p2 `1 ) + g ;
A117: a2 `1 = x1 by A114, EUCLID:56;
( ((p2 `1 ) - g) + g < x1 + g & (p2 `1 ) - x1 > (p2 `1 ) - ((p2 `1 ) + g) ) by A115, A116, XREAL_1:8, XREAL_1:17;
then ( (p2 `1 ) - x1 < (x1 + g) - x1 & (p2 `1 ) - x1 > - g ) by XREAL_1:11;
then abs ((p2 `1 ) - x1) < g by SEQ_2:9;
then abs (- ((p2 `1 ) - x1)) < g by COMPLEX1:138;
then abs (x1 - (p2 `1 )) < g ;
then a2 `1 in ].((p2 `1 ) - g),((p2 `1 ) + g).[ by A117, RCOMP_1:8;
hence b in V by A108, A111, A113; :: thesis:

end;

then fX2 is continuous by JGRAPH_2:20;
then reconsider fx2 = fx2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by TOPREAL6:83;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st fY2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )

proof

let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis:
let V be Subset of R^1 ; :: thesis:
assume that
A118: fY2 . p in V and
A119: V is open ; :: thesis:
consider p1, p2 being Point of (TOP-REAL 2) such that
A120: p = [p1,p2] and
A121: fY2 . p = p2 `2 by A28;
reconsider V1 = V as open Subset of REAL by A119, BORSUK_5:62, TOPMETR:24;
consider g being real number such that
A122: 0 < g and
A123: ].((p2 `2 ) - g),((p2 `2 ) + g).[ c= V1 by A118, A121, RCOMP_1:40;
reconsider g = g as Element of REAL by XREAL_0:def 1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } c= the carrier of (TOP-REAL 2)

proof

end;

then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2 ) - g < y & y < (p2 `2 ) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W1:] ; :: thesis:
A124: p2 = |[(p2 `1 ),(p2 `2 )]| by EUCLID:57;
( (p2 `2 ) - g < (p2 `2 ) - 0 & (p2 `2 ) + 0 < (p2 `2 ) + g ) by A122, XREAL_1:8, XREAL_1:17;
then p2 in W1 by A124;
hence p in [:([#] (TOP-REAL 2)),W1:] by A120, ZFMISC_1:def 2; :: thesis:
W1 is open by PSCOMP_1:68;
hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:46; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in fY2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis:
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A125: a in [:([#] (TOP-REAL 2)),W1:] and
A126: fY2 . a = b by FUNCT_2:116;
consider a1, a2 being Point of (TOP-REAL 2) such that
A127: a = [a1,a2] and
A128: fY2 . a = a2 `2 by A28;
a2 in W1 by A125, A127, ZFMISC_1:106;
then consider x1, y1 being Element of REAL such that
A129: a2 = |[x1,y1]| and
A130: (p2 `2 ) - g < y1 and
A131: y1 < (p2 `2 ) + g ;
A132: a2 `2 = y1 by A129, EUCLID:56;
( ((p2 `2 ) - g) + g < y1 + g & (p2 `2 ) - y1 > (p2 `2 ) - ((p2 `2 ) + g) ) by A130, A131, XREAL_1:8, XREAL_1:17;
then ( (p2 `2 ) - y1 < (y1 + g) - y1 & (p2 `2 ) - y1 > - g ) by XREAL_1:11;
then abs ((p2 `2 ) - y1) < g by SEQ_2:9;
then abs (- ((p2 `2 ) - y1)) < g by COMPLEX1:138;
then abs (y1 - (p2 `2 )) < g ;
then a2 `2 in ].((p2 `2 ) - g),((p2 `2 ) + g).[ by A132, RCOMP_1:8;
hence b in V by A123, A126, A128; :: thesis:

end;

then fY2 is continuous by JGRAPH_2:20;
then reconsider fy2 = fy2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by TOPREAL6:83;
reconsider rr = r ^2 as Real by XREAL_0:def 1;
set f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr;
reconsider f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by Lm1;
set Zf1 = f1 | OK;
set Zfx2 = fx2 | OK;
set Zfy2 = fy2 | OK;
set Zdx = dx | OK;
set Zdy = dy | OK;
set Zxo = xo | OK;
set Zyo = yo | OK;
set xx = (xo | OK) (#) (dx | OK);
set yy = (yo | OK) (#) (dy | OK);
set m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK));
A133: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) = OK by PRE_TOPC:29;
A134: for y, z being Point of (Tdisk o,r) st y <> z holds
[y,z] in OK

proof

let y, z be Point of (Tdisk o,r); :: thesis:
assume A135: y <> z ; :: thesis:
( y is Point of (TOP-REAL 2) & z is Point of (TOP-REAL 2) ) by PRE_TOPC:55;
then [y,z] in DiffElems (TOP-REAL 2),(TOP-REAL 2) by A135;
hence [y,z] in OK by XBOOLE_0:def 4; :: thesis:

end;

now

let b be real number ; :: thesis:
assume b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) ; :: thesis:
then consider a being set such that
A136: a in dom (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) and
A137: (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . a = b by FUNCT_1:def 5;
a in DiffElems (TOP-REAL 2),(TOP-REAL 2) by A133, A136, XBOOLE_0:def 4;
then consider y, z being Point of (TOP-REAL 2) such that
A138: a = [y,z] and
A139: y <> z ;
a in the carrier of [:(Tdisk o,r),(Tdisk o,r):] by A133, A136, XBOOLE_0:def 4;
then consider a1, a2 being Point of (Tdisk o,r) such that
A140: a = [a1,a2] by BORSUK_1:50;
A141: ( a1 = y & a2 = z ) by A138, A140, ZFMISC_1:33;
consider x3, x4 being Point of (TOP-REAL 2) such that
A142: [y,z] = [x3,x4] and
A143: dx . [y,z] = (x3 `1 ) - (x4 `1 ) by A19;
A144: ( y = x3 & z = x4 ) by A142, ZFMISC_1:33;
consider x5, x6 being Point of (TOP-REAL 2) such that
A145: [y,z] = [x5,x6] and
A146: dy . [y,z] = (x5 `2 ) - (x6 `2 ) by A22;
A147: ( y = x5 & z = x6 ) by A145, ZFMISC_1:33;
set r1 = (y `1 ) - (z `1 );
set r2 = (y `2 ) - (z `2 );
A148: (dx | OK) . [y,z] = dx . [y,z] by A134, A139, A141, FUNCT_1:72;
A149: (dy | OK) . [y,z] = dy . [y,z] by A134, A139, A141, FUNCT_1:72;
A150: (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A136, A138, VALUED_1:1
.= (((dx | OK) . [y,z]) * ((dx | OK) . [y,z])) + (((dy | OK) (#) (dy | OK)) . [y,z]) by VALUED_1:5
.= (((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ) by A143, A144, A146, A147, A148, A149, VALUED_1:5 ;

now

assume (((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ) = 0 ; :: thesis:
then ( (y `1 ) - (z `1 ) = 0 & (y `2 ) - (z `2 ) = 0 ) by COMPLEX1:2;
hence contradiction by A139, TOPREAL3:11; :: thesis:

end;

hence 0 < b by A137, A138, A150; :: thesis:

end;

now

let b be real number ; :: thesis:
assume b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) ; :: thesis:
then consider a being set such that
A153: a in dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) and
A154: ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . a = b by FUNCT_1:def 5;
a in DiffElems (TOP-REAL 2),(TOP-REAL 2) by A133, A153, XBOOLE_0:def 4;
then consider y, z being Point of (TOP-REAL 2) such that
A155: a = [y,z] and
A156: y <> z ;
set r3 = (z `1 ) - (o `1 );
set r4 = (z `2 ) - (o `2 );
a in the carrier of [:(Tdisk o,r),(Tdisk o,r):] by A133, A153, XBOOLE_0:def 4;
then consider a1, a2 being Point of (Tdisk o,r) such that
A157: a = [a1,a2] by BORSUK_1:50;
A158: ( a1 = y & a2 = z ) by A155, A157, ZFMISC_1:33;
then A159: (f1 | OK) . [y,z] = f1 . [y,z] by A134, A156, FUNCT_1:72;
A160: (xo | OK) . [y,z] = xo . [y,z] by A134, A156, A158, FUNCT_1:72;
A161: (yo | OK) . [y,z] = yo . [y,z] by A134, A156, A158, FUNCT_1:72;
consider x9, x10 being Point of (TOP-REAL 2) such that
A162: [y,z] = [x9,x10] and
A163: xo . [y,z] = (x10 `1 ) - (o `1 ) by A13;
A164: ( y = x9 & z = x10 ) by A162, ZFMISC_1:33;
consider x11, x12 being Point of (TOP-REAL 2) such that
A165: [y,z] = [x11,x12] and
A166: yo . [y,z] = (x12 `2 ) - (o `2 ) by A16;
A167: ( y = x11 & z = x12 ) by A165, ZFMISC_1:33;
A168: ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A153, A155, VALUED_1:13
.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2 ) by A159, FUNCOP_1:13
.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2 ) by A153, A155, VALUED_1:1
.= ((((xo | OK) . [y,z]) * ((xo | OK) . [y,z])) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2 ) by VALUED_1:5
.= ((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 ) by A160, A161, A163, A164, A166, A167, VALUED_1:5 ;
the carrier of (Tdisk o,r) = cl_Ball o,r by Th3;
then |.(z - o).| <= r by A158, TOPREAL9:8;
then A169: |.(z - o).| ^2 <= r ^2 by SQUARE_1:77;
|.(z - o).| ^2 = (((z - o) `1 ) ^2 ) + (((z - o) `2 ) ^2 ) by JGRAPH_1:46
.= (((z `1 ) - (o `1 )) ^2 ) + (((z - o) `2 ) ^2 ) by TOPREAL3:8
.= (((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 ) by TOPREAL3:8 ;
then ((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 ) <= (r ^2 ) - (r ^2 ) by A169, XREAL_1:11;
hence 0 >= b by A154, A155, A168; :: thesis:

end;

proof

let x be Point of (Tdisk o,r); :: thesis:
A171: not x is_a_fixpoint_of f by A10, ABIAN:def 5;
then consider y, z being Point of (TOP-REAL 2) such that
A172: y = x and
A173: z = f . x and
A174: HC x,f = HC z,y,o,r by Def4;
A175: x <> f . x by A171, ABIAN:def 4;
then [x,(f . x)] in DiffElems (TOP-REAL 2),(TOP-REAL 2) by A172, A173;
then A176: [y,z] in OK by A172, A173, XBOOLE_0:def 4;
set r1 = (y `1 ) - (z `1 );
set r2 = (y `2 ) - (z `2 );
set r3 = (z `1 ) - (o `1 );
set r4 = (z `2 ) - (o `2 );
set l = ((- ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 ))))) + (sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ));
consider x1, x2 being Point of (TOP-REAL 2) such that
A177: [y,z] = [x1,x2] and
A178: fx2 . [y,z] = x2 `1 by A25;
A179: z = x2 by A177, ZFMISC_1:33;
consider x7, x8 being Point of (TOP-REAL 2) such that
A180: [y,z] = [x7,x8] and
A181: fy2 . [y,z] = x8 `2 by A28;
A182: z = x8 by A180, ZFMISC_1:33;
consider x3, x4 being Point of (TOP-REAL 2) such that
A183: [y,z] = [x3,x4] and
A184: dx . [y,z] = (x3 `1 ) - (x4 `1 ) by A19;
A185: ( y = x3 & z = x4 ) by A183, ZFMISC_1:33;
consider x5, x6 being Point of (TOP-REAL 2) such that
A186: [y,z] = [x5,x6] and
A187: dy . [y,z] = (x5 `2 ) - (x6 `2 ) by A22;
A188: ( y = x5 & z = x6 ) by A186, ZFMISC_1:33;
consider x9, x10 being Point of (TOP-REAL 2) such that
A189: [y,z] = [x9,x10] and
A190: xo . [y,z] = (x10 `1 ) - (o `1 ) by A13;
A191: ( y = x9 & z = x10 ) by A189, ZFMISC_1:33;
consider x11, x12 being Point of (TOP-REAL 2) such that
A192: [y,z] = [x11,x12] and
A193: yo . [y,z] = (x12 `2 ) - (o `2 ) by A16;
A194: ( y = x11 & z = x12 ) by A192, ZFMISC_1:33;
A195: dom X3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;
A196: dom Y3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;
A197: dom (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;
A198: (dx | OK) . [y,z] = dx . [y,z] by A134, A172, A173, A175, FUNCT_1:72;
A199: (dy | OK) . [y,z] = dy . [y,z] by A134, A172, A173, A175, FUNCT_1:72;
A200: (f1 | OK) . [y,z] = f1 . [y,z] by A134, A172, A173, A175, FUNCT_1:72;
A201: (xo | OK) . [y,z] = xo . [y,z] by A134, A172, A173, A175, FUNCT_1:72;
A202: (yo | OK) . [y,z] = yo . [y,z] by A134, A172, A173, A175, FUNCT_1:72;
A203: m . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A133, A176, VALUED_1:1
.= (((dx | OK) . [y,z]) * ((dx | OK) . [y,z])) + (((dy | OK) (#) (dy | OK)) . [y,z]) by VALUED_1:5
.= (((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ) by A184, A185, A187, A188, A198, A199, VALUED_1:5 ;
A204: ((xo | OK) (#) (dx | OK)) . [y,z] = ((xo | OK) . [y,z]) * ((dx | OK) . [y,z]) by VALUED_1:5;
A205: ((yo | OK) (#) (dy | OK)) . [y,z] = ((yo | OK) . [y,z]) * ((dy | OK) . [y,z]) by VALUED_1:5;
A206: (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) . [y,z] = (((xo | OK) (#) (dx | OK)) . [y,z]) + (((yo | OK) (#) (dy | OK)) . [y,z]) by A133, A176, VALUED_1:1;
then A207: ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z] = ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 by A184, A185, A187, A188, A190, A191, A193, A194, A198, A199, A201, A202, A204, A205, VALUED_1:5;
A208: p2 . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A133, A152, A176, VALUED_1:13
.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2 ) by A200, FUNCOP_1:13
.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2 ) by A133, A176, VALUED_1:1
.= ((((xo | OK) . [y,z]) * ((xo | OK) . [y,z])) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2 ) by VALUED_1:5
.= ((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 ) by A190, A191, A193, A194, A201, A202, VALUED_1:5 ;
dom (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;
then A209: (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [y,z] = sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) . [y,z]) by A133, A176, PARTFUN3:def 5
.= sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z]) - ((m (#) p2) . [y,z])) by A133, A176, A197, VALUED_1:13
.= sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))) by A203, A207, A208, VALUED_1:5 ;
dom (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;
then A210: (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) . [y,z] = (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [y,z]) * ((m . [y,z]) " ) by A133, A176, RFUNCT_1:def 4
.= (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [y,z]) / (m . [y,z]) by XCMPLX_0:def 9
.= (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z]) + ((sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [y,z])) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) by A133, A176, A203, VALUED_1:1
.= ((- ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 ))))) + (sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) by A184, A185, A187, A188, A190, A191, A193, A194, A198, A199, A201, A202, A204, A205, A206, A209, VALUED_1:8 ;
A211: X3 . [y,z] = ((fx2 | OK) . [y,z]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [y,z]) by A133, A176, VALUED_1:1
.= (z `1 ) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [y,z]) by A134, A172, A173, A175, A178, A179, FUNCT_1:72
.= (z `1 ) + ((((- ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 ))))) + (sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ))) * ((y `1 ) - (z `1 ))) by A184, A185, A198, A210, VALUED_1:5 ;
A212: Y3 . [y,z] = ((fy2 | OK) . [y,z]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [y,z]) by A133, A176, VALUED_1:1
.= (z `2 ) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [y,z]) by A134, A172, A173, A175, A181, A182, FUNCT_1:72
.= (z `2 ) + ((((- ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 ))))) + (sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ))) * ((y `2 ) - (z `2 ))) by A187, A188, A199, A210, VALUED_1:5 ;
thus (BR-map f) . x = HC x,f by Def5
.= |[((z `1 ) + ((((- ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 ))))) + (sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ))) * ((y `1 ) - (z `1 )))),((z `2 ) + ((((- ((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 ))))) + (sqrt ((((((z `1 ) - (o `1 )) * ((y `1 ) - (z `1 ))) + (((z `2 ) - (o `2 )) * ((y `2 ) - (z `2 )))) ^2 ) - (((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 )) * (((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (z `1 )) ^2 ) + (((y `2 ) - (z `2 )) ^2 ))) * ((y `2 ) - (z `2 ))))]| by A172, A173, A174, A175, Th8
.= R2Homeomorphism . [(X3 . [y,z]),(Y3 . [y,z])] by A211, A212, TOPREALA:def 2
.= R2Homeomorphism . (<:X3,Y3:> . [y,z]) by A133, A176, A195, A196, FUNCT_3:69
.= (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] by A133, A172, A173, A176, FUNCT_2:21 ; :: thesis:

end;

( X3 is continuous & Y3 is continuous ) by TOPREAL6:83;
then reconsider F = <:X3,Y3:> as continuous Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[:R^1 ,R^1 :] by YELLOW12:41;
for p being Point of (Tdisk o,r)
for V being Subset of (Tcircle o,r) st (BR-map f) . p in V & V is open holds
ex W being Subset of (Tdisk o,r) st
( p in W & W is open & (BR-map f) .: W c= V )

proof

let p be Point of (Tdisk o,r); :: thesis:
let V be Subset of (Tcircle o,r); :: thesis:
assume that
A213: (BR-map f) . p in V and
A214: V is open ; :: thesis:
reconsider p1 = p, fp = f . p as Point of (TOP-REAL 2) by PRE_TOPC:55;
not p is_a_fixpoint_of f by A10, ABIAN:def 5;
then p <> f . p by ABIAN:def 4;
then [p1,fp] in DiffElems (TOP-REAL 2),(TOP-REAL 2) ;
then A215: [p,(f . p)] in OK by XBOOLE_0:def 4;
consider V1 being Subset of (TOP-REAL 2) such that
A216: V1 is open and
A217: V1 /\ ([#] (Tcircle o,r)) = V by A214, TOPS_2:32;
A218: (BR-map f) . p = (R2Homeomorphism * F) . [p,(f . p)] by A170;
R2Homeomorphism " is being_homeomorphism by TOPREALA:56, TOPS_2:70;
then A219: (R2Homeomorphism " ) .: V1 is open by A216, TOPGRP_1:25;
A220: dom F = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;
A221: dom R2Homeomorphism = the carrier of [:R^1 ,R^1 :] by FUNCT_2:def 1;
then A222: rng F c= dom R2Homeomorphism ;
then A223: dom (R2Homeomorphism * F) = dom F by RELAT_1:46;
A224: ( rng R2Homeomorphism = [#] (TOP-REAL 2) & R2Homeomorphism is one-to-one ) by TOPREALA:56, TOPS_2:def 5;
A225: (R2Homeomorphism " ) * (R2Homeomorphism * F) = ((R2Homeomorphism " ) * R2Homeomorphism ) * F by RELAT_1:55
.= (id (dom R2Homeomorphism )) * F by A224, TOPS_2:65 ;
dom (id (dom R2Homeomorphism )) = dom R2Homeomorphism by RELAT_1:71;
then A226: dom ((id (dom R2Homeomorphism )) * F) = dom F by A222, RELAT_1:46;
for x being set st x in dom F holds
((id (dom R2Homeomorphism )) * F) . x = F . x

proof

let x be set ; :: thesis:
assume A227: x in dom F ; :: thesis:
A228: F . x in rng F by A227, FUNCT_1:def 5;
thus ((id (dom R2Homeomorphism )) * F) . x = (id (dom R2Homeomorphism )) . (F . x) by A227, FUNCT_1:23
.= F . x by A221, A228, FUNCT_1:35 ; :: thesis:

end;

then A229: (id (dom R2Homeomorphism )) * F = F by A226, FUNCT_1:9;
(R2Homeomorphism * F) . [p1,fp] in V1 by A213, A217, A218, XBOOLE_0:def 4;
then (R2Homeomorphism " ) . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism " ) .: V1 by FUNCT_2:43;
then ((R2Homeomorphism " ) * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism " ) .: V1 by A133, A215, A220, A223, FUNCT_1:23;
then consider W being Subset of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) such that
A230: [p1,fp] in W and
A231: W is open and
A232: F .: W c= (R2Homeomorphism " ) .: V1 by A133, A215, A219, A225, A229, JGRAPH_2:20;
consider WW being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A233: WW is open and
A234: WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) = W by A231, TOPS_2:32;
consider SF being Subset-Family of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A235: WW = union SF and
A236: for e being set st e in SF holds
ex X1, Y1 being Subset of (TOP-REAL 2) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by A233, BORSUK_1:45;
[p1,fp] in WW by A230, A234, XBOOLE_0:def 4;
then consider Z being set such that
A237: [p1,fp] in Z and
A238: Z in SF by A235, TARSKI:def 4;
consider X1, Y1 being Subset of (TOP-REAL 2) such that
A239: Z = [:X1,Y1:] and
A240: X1 is open and
A241: Y1 is open by A236, A238;
set ZZ = Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK));
reconsider XX = X1 /\ ([#] (Tdisk o,r)), YY = Y1 /\ ([#] (Tdisk o,r)) as open Subset of (Tdisk o,r) by A240, A241, TOPS_2:32;
fp in Y1 by A237, A239, ZFMISC_1:106;
then fp in YY by XBOOLE_0:def 4;
then consider M being Subset of (Tdisk o,r) such that
A242: p in M and
A243: M is open and
A244: f .: M c= YY by JGRAPH_2:20;
take W1 = XX /\ M; :: thesis:
p in X1 by A237, A239, ZFMISC_1:106;
then p in XX by XBOOLE_0:def 4;
hence p in W1 by A242, XBOOLE_0:def 4; :: thesis:
thus W1 is open by A243, TOPS_1:38; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in (BR-map f) .: W1 ; :: thesis:
then consider a being Point of (Tdisk o,r) such that
A245: a in W1 and
A246: b = (BR-map f) . a by FUNCT_2:116;
reconsider a1 = a, fa = f . a as Point of (TOP-REAL 2) by PRE_TOPC:55;
a in XX by A245, XBOOLE_0:def 4;
then A247: a in X1 by XBOOLE_0:def 4;
not a is_a_fixpoint_of f by A10, ABIAN:def 5;
then a <> f . a by ABIAN:def 4;
then [a1,fa] in DiffElems (TOP-REAL 2),(TOP-REAL 2) ;
then A248: [a,(f . a)] in OK by XBOOLE_0:def 4;
a in M by A245, XBOOLE_0:def 4;
then fa in f .: M by FUNCT_2:43;
then f . a in Y1 by A244, XBOOLE_0:def 4;
then [a,fa] in Z by A239, A247, ZFMISC_1:def 2;
then [a,fa] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by A133, A248, XBOOLE_0:def 4;
then A249: F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) by FUNCT_2:43;
A250: R2Homeomorphism " = R2Homeomorphism " by A224, TOPS_2:def 4;
A251: dom (R2Homeomorphism " ) = [#] (TOP-REAL 2) by A224, TOPS_2:62;
Z c= WW by A235, A238, ZFMISC_1:92;
then Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by XBOOLE_1:27;
then F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) c= F .: W by A234, RELAT_1:156;
then F . [a1,fa] in F .: W by A249;
then R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism " ) .: V1) by A232, FUNCT_2:43;
then (R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism " ) .: V1) by A133, A248, FUNCT_2:21;
then (R2Homeomorphism * F) . [a1,fa] in V1 by A224, A250, A251, PARTFUN3:1;
then (BR-map f) . a in V1 by A170;
hence b in V by A217, A246, XBOOLE_0:def 4; :: thesis:

end;

hence BR-map f is continuous by JGRAPH_2:20; :: thesis: