set R = R2Homeomorphism ;

defpred S_{1}[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st

( $1 = [x1,x2] & $2 = x2 `1 );

defpred S_{2}[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st

( $1 = [x1,x2] & $2 = (x1 `1) - (x2 `1) );

let r be positive Real; :: thesis: for o being Point of (TOP-REAL 2)

for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds

BR-map f is continuous

let o be Point of (TOP-REAL 2); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds

BR-map f is continuous

defpred S_{3}[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st

( $1 = [x1,x2] & $2 = (x2 `1) - (o `1) );

defpred S_{4}[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st

( $1 = [x1,x2] & $2 = (x2 `2) - (o `2) );

reconsider rr = r ^2 as Element of REAL by XREAL_0:def 1;

set f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr;

A1: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S_{3}[x,r]

A3: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S_{3}[x,xo . x]
from FUNCT_2:sch 3(A1);

A4: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S_{1}[x,r]

A6: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S_{1}[x,fx2 . x]
from FUNCT_2:sch 3(A4);

A7: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S_{4}[x,r]

A9: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S_{4}[x,yo . x]
from FUNCT_2:sch 3(A7);

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 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)):];

set s = the Point of (Tcircle (o,r));

A10: |.(o - o).| = |.(0. (TOP-REAL 2)).| by RLVECT_1:5

.= 0 by TOPRNS_1:23 ;

A11: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;

then A14: o is Point of (Tdisk (o,r)) by A10, TOPREAL9:8;

( the Point of (Tcircle (o,r)) in the carrier of (Tcircle (o,r)) & Sphere (o,r) c= cl_Ball (o,r) ) by TOPREAL9:17;

then the Point of (Tcircle (o,r)) is Point of (Tdisk (o,r)) by A11, Th3;

then [o, the Point of (Tcircle (o,r))] in [: the carrier of (Tdisk (o,r)), the carrier of (Tdisk (o,r)):] by A14, ZFMISC_1:87;

then A15: [o, the Point of (Tcircle (o,r))] in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by BORSUK_1:def 2;

the Point of (Tcircle (o,r)) is Point of (TOP-REAL 2) by PRE_TOPC:25;

then [o, the Point of (Tcircle (o,r))] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A12;

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 A15, XBOOLE_0:def 4;

set Zf1 = f1 | OK;

defpred S_{5}[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st

( $1 = [x1,x2] & $2 = x2 `2 );

defpred S_{6}[ set , set ] means ex y1, y2 being Point of (TOP-REAL 2) st

( $1 = [y1,y2] & $2 = (y1 `2) - (y2 `2) );

set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | OK;

let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: ( f is without_fixpoints implies BR-map f is continuous )

assume A16: f is without_fixpoints ; :: thesis: BR-map f is continuous

A17: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S_{6}[x,r]

A19: for y being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S_{6}[y,dy . y]
from FUNCT_2:sch 3(A17);

A20: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S_{5}[x,r]

A22: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S_{5}[x,fy2 . x]
from FUNCT_2:sch 3(A20);

A23: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S_{2}[x,r]

A25: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S_{2}[x,dx . x]
from FUNCT_2:sch 3(A23);

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:17;

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 )

then reconsider yo = yo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

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 )

then reconsider xo = xo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

set Zyo = yo | OK;

set Zxo = xo | OK;

set p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK);

set g = BR-map f;

A52: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) = OK by PRE_TOPC:8;

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 )

then reconsider dy = dy as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

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 )

then reconsider dx = dx as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

set Zdy = dy | OK;

set Zdx = dx | OK;

set m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK));

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 )

then reconsider fy2 = fy2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

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 )

then reconsider fx2 = fx2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

set yy = (yo | OK) (#) (dy | OK);

set xx = (xo | OK) (#) (dx | OK);

set Zfy2 = fy2 | OK;

set Zfx2 = fx2 | OK;

set p1 = (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)));

A139: dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;

A140: for y, z being Point of (Tdisk (o,r)) st y <> z holds

[y,z] in OK

reconsider p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK) as nonpositive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A142, PARTFUN3:def 3;

set pp = ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2);

set k = ((- (((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;

set x3 = (fx2 | OK) + ((((- (((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));

set y3 = (fy2 | OK) + ((((- (((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));

reconsider X3 = (fx2 | OK) + ((((- (((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)), Y3 = (fy2 | OK) + ((((- (((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)) as Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),R^1 by TOPMETR:17;

set F = <:X3,Y3:>;

A175: for x being Point of (Tdisk (o,r)) holds (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)]

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 )

defpred S

( $1 = [x1,x2] & $2 = x2 `1 );

defpred S

( $1 = [x1,x2] & $2 = (x1 `1) - (x2 `1) );

let r be positive Real; :: thesis: for o being Point of (TOP-REAL 2)

for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds

BR-map f is continuous

let o be Point of (TOP-REAL 2); :: thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds

BR-map f is continuous

defpred S

( $1 = [x1,x2] & $2 = (x2 `1) - (o `1) );

defpred S

( $1 = [x1,x2] & $2 = (x2 `2) - (o `2) );

reconsider rr = r ^2 as Element of REAL by XREAL_0:def 1;

set f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr;

A1: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S

proof

consider xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S_{3}[x,r]

consider x1, x2 being Point of (TOP-REAL 2) such that

A2: x = [x1,x2] by BORSUK_1:10;

reconsider x2o = (x2 `1) - (o `1) as Element of REAL by XREAL_0:def 1;

take x2o ; :: thesis: S_{3}[x,x2o]

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x2o = (x2 `1) - (o `1) )

take x2 ; :: thesis: ( x = [x1,x2] & x2o = (x2 `1) - (o `1) )

thus ( x = [x1,x2] & x2o = (x2 `1) - (o `1) ) by A2; :: thesis: verum

end;consider x1, x2 being Point of (TOP-REAL 2) such that

A2: x = [x1,x2] by BORSUK_1:10;

reconsider x2o = (x2 `1) - (o `1) as Element of REAL by XREAL_0:def 1;

take x2o ; :: thesis: S

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x2o = (x2 `1) - (o `1) )

take x2 ; :: thesis: ( x = [x1,x2] & x2o = (x2 `1) - (o `1) )

thus ( x = [x1,x2] & x2o = (x2 `1) - (o `1) ) by A2; :: thesis: verum

A3: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S

A4: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S

proof

consider fx2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S_{1}[x,r]

consider x1, x2 being Point of (TOP-REAL 2) such that

A5: x = [x1,x2] by BORSUK_1:10;

reconsider x21 = x2 `1 as Element of REAL by XREAL_0:def 1;

take x21 ; :: thesis: S_{1}[x,x21]

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x21 = x2 `1 )

take x2 ; :: thesis: ( x = [x1,x2] & x21 = x2 `1 )

thus ( x = [x1,x2] & x21 = x2 `1 ) by A5; :: thesis: verum

end;consider x1, x2 being Point of (TOP-REAL 2) such that

A5: x = [x1,x2] by BORSUK_1:10;

reconsider x21 = x2 `1 as Element of REAL by XREAL_0:def 1;

take x21 ; :: thesis: S

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x21 = x2 `1 )

take x2 ; :: thesis: ( x = [x1,x2] & x21 = x2 `1 )

thus ( x = [x1,x2] & x21 = x2 `1 ) by A5; :: thesis: verum

A6: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S

A7: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S

proof

consider yo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S_{4}[x,r]

consider x1, x2 being Point of (TOP-REAL 2) such that

A8: x = [x1,x2] by BORSUK_1:10;

reconsider x2o = (x2 `2) - (o `2) as Element of REAL by XREAL_0:def 1;

take x2o ; :: thesis: S_{4}[x,x2o]

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x2o = (x2 `2) - (o `2) )

take x2 ; :: thesis: ( x = [x1,x2] & x2o = (x2 `2) - (o `2) )

thus ( x = [x1,x2] & x2o = (x2 `2) - (o `2) ) by A8; :: thesis: verum

end;consider x1, x2 being Point of (TOP-REAL 2) such that

A8: x = [x1,x2] by BORSUK_1:10;

reconsider x2o = (x2 `2) - (o `2) as Element of REAL by XREAL_0:def 1;

take x2o ; :: thesis: S

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x2o = (x2 `2) - (o `2) )

take x2 ; :: thesis: ( x = [x1,x2] & x2o = (x2 `2) - (o `2) )

thus ( x = [x1,x2] & x2o = (x2 `2) - (o `2) ) by A8; :: thesis: verum

A9: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S

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 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)):];

set s = the Point of (Tcircle (o,r));

A10: |.(o - o).| = |.(0. (TOP-REAL 2)).| by RLVECT_1:5

.= 0 by TOPRNS_1:23 ;

A11: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;

A12: now :: thesis: not o = the Point of (Tcircle (o,r))

the carrier of (Tdisk (o,r)) = cl_Ball (o,r)
by Th3;assume A13:
o = the Point of (Tcircle (o,r))
; :: thesis: contradiction

( Ball (o,r) misses Sphere (o,r) & o in Ball (o,r) ) by A10, TOPREAL9:7, TOPREAL9:19;

hence contradiction by A11, A13, XBOOLE_0:3; :: thesis: verum

end;( Ball (o,r) misses Sphere (o,r) & o in Ball (o,r) ) by A10, TOPREAL9:7, TOPREAL9:19;

hence contradiction by A11, A13, XBOOLE_0:3; :: thesis: verum

then A14: o is Point of (Tdisk (o,r)) by A10, TOPREAL9:8;

( the Point of (Tcircle (o,r)) in the carrier of (Tcircle (o,r)) & Sphere (o,r) c= cl_Ball (o,r) ) by TOPREAL9:17;

then the Point of (Tcircle (o,r)) is Point of (Tdisk (o,r)) by A11, Th3;

then [o, the Point of (Tcircle (o,r))] in [: the carrier of (Tdisk (o,r)), the carrier of (Tdisk (o,r)):] by A14, ZFMISC_1:87;

then A15: [o, the Point of (Tcircle (o,r))] in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by BORSUK_1:def 2;

the Point of (Tcircle (o,r)) is Point of (TOP-REAL 2) by PRE_TOPC:25;

then [o, the Point of (Tcircle (o,r))] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A12;

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 A15, XBOOLE_0:def 4;

set Zf1 = f1 | OK;

defpred S

( $1 = [x1,x2] & $2 = x2 `2 );

defpred S

( $1 = [y1,y2] & $2 = (y1 `2) - (y2 `2) );

set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | OK;

let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); :: thesis: ( f is without_fixpoints implies BR-map f is continuous )

assume A16: f is without_fixpoints ; :: thesis: BR-map f is continuous

A17: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S

proof

consider dy being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S_{6}[x,r]

consider x1, x2 being Point of (TOP-REAL 2) such that

A18: x = [x1,x2] by BORSUK_1:10;

reconsider x12 = (x1 `2) - (x2 `2) as Element of REAL by XREAL_0:def 1;

take x12 ; :: thesis: S_{6}[x,x12]

take x1 ; :: thesis: ex y2 being Point of (TOP-REAL 2) st

( x = [x1,y2] & x12 = (x1 `2) - (y2 `2) )

take x2 ; :: thesis: ( x = [x1,x2] & x12 = (x1 `2) - (x2 `2) )

thus ( x = [x1,x2] & x12 = (x1 `2) - (x2 `2) ) by A18; :: thesis: verum

end;consider x1, x2 being Point of (TOP-REAL 2) such that

A18: x = [x1,x2] by BORSUK_1:10;

reconsider x12 = (x1 `2) - (x2 `2) as Element of REAL by XREAL_0:def 1;

take x12 ; :: thesis: S

take x1 ; :: thesis: ex y2 being Point of (TOP-REAL 2) st

( x = [x1,y2] & x12 = (x1 `2) - (y2 `2) )

take x2 ; :: thesis: ( x = [x1,x2] & x12 = (x1 `2) - (x2 `2) )

thus ( x = [x1,x2] & x12 = (x1 `2) - (x2 `2) ) by A18; :: thesis: verum

A19: for y being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S

A20: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S

proof

consider fy2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S_{5}[x,r]

consider x1, x2 being Point of (TOP-REAL 2) such that

A21: x = [x1,x2] by BORSUK_1:10;

reconsider x22 = x2 `2 as Element of REAL by XREAL_0:def 1;

take x22 ; :: thesis: S_{5}[x,x22]

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x22 = x2 `2 )

take x2 ; :: thesis: ( x = [x1,x2] & x22 = x2 `2 )

thus ( x = [x1,x2] & x22 = x2 `2 ) by A21; :: thesis: verum

end;consider x1, x2 being Point of (TOP-REAL 2) such that

A21: x = [x1,x2] by BORSUK_1:10;

reconsider x22 = x2 `2 as Element of REAL by XREAL_0:def 1;

take x22 ; :: thesis: S

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x22 = x2 `2 )

take x2 ; :: thesis: ( x = [x1,x2] & x22 = x2 `2 )

thus ( x = [x1,x2] & x22 = x2 `2 ) by A21; :: thesis: verum

A22: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S

A23: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Element of REAL st S

proof

consider dx being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S_{2}[x,r]

consider x1, x2 being Point of (TOP-REAL 2) such that

A24: x = [x1,x2] by BORSUK_1:10;

reconsider x12 = (x1 `1) - (x2 `1) as Element of REAL by XREAL_0:def 1;

take x12 ; :: thesis: S_{2}[x,x12]

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x12 = (x1 `1) - (x2 `1) )

take x2 ; :: thesis: ( x = [x1,x2] & x12 = (x1 `1) - (x2 `1) )

thus ( x = [x1,x2] & x12 = (x1 `1) - (x2 `1) ) by A24; :: thesis: verum

end;consider x1, x2 being Point of (TOP-REAL 2) such that

A24: x = [x1,x2] by BORSUK_1:10;

reconsider x12 = (x1 `1) - (x2 `1) as Element of REAL by XREAL_0:def 1;

take x12 ; :: thesis: S

take x1 ; :: thesis: ex x2 being Point of (TOP-REAL 2) st

( x = [x1,x2] & x12 = (x1 `1) - (x2 `1) )

take x2 ; :: thesis: ( x = [x1,x2] & x12 = (x1 `1) - (x2 `1) )

thus ( x = [x1,x2] & x12 = (x1 `1) - (x2 `1) ) by A24; :: thesis: verum

A25: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S

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:17;

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

then
Yo is continuous
by JGRAPH_2:10;
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( Yo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Yo .: W c= V ) )

assume that

A26: Yo . p in V and

A27: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Yo .: W c= V )

reconsider V1 = V as open Subset of REAL by A27, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A28: p = [p1,p2] and

A29: Yo . p = (p2 `2) - (o `2) by A9;

set r = (p2 `2) - (o `2);

consider g being Real such that

A30: 0 < g and

A31: ].(((p2 `2) - (o `2)) - g),(((p2 `2) - (o `2)) + g).[ c= V1 by A26, A29, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2)

take [:([#] (TOP-REAL 2)),W2:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )

A32: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A30, XREAL_1:6, XREAL_1:15;

then p2 in W2 by A32;

hence p in [:([#] (TOP-REAL 2)),W2:] by A28, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )

W2 is open by PSCOMP_1:21;

hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; :: thesis: Yo .: [:([#] (TOP-REAL 2)),W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Yo .: [:([#] (TOP-REAL 2)),W2:] or b in V )

assume b in Yo .: [:([#] (TOP-REAL 2)),W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A33: a in [:([#] (TOP-REAL 2)),W2:] and

A34: Yo . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A35: a = [a1,a2] and

A36: yo . a = (a2 `2) - (o `2) by A9;

a2 in W2 by A33, A35, ZFMISC_1:87;

then consider x2, y2 being Real such that

A37: a2 = |[x2,y2]| and

A38: ( (p2 `2) - g < y2 & y2 < (p2 `2) + g ) ;

a2 `2 = y2 by A37, EUCLID:52;

then ( ((p2 `2) - g) - (o `2) < (a2 `2) - (o `2) & (a2 `2) - (o `2) < ((p2 `2) + g) - (o `2) ) by A38, XREAL_1:9;

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 A31, A34, A36; :: thesis: verum

end;ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Yo .: W c= V )

let V be Subset of R^1; :: thesis: ( Yo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Yo .: W c= V ) )

assume that

A26: Yo . p in V and

A27: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Yo .: W c= V )

reconsider V1 = V as open Subset of REAL by A27, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A28: p = [p1,p2] and

A29: Yo . p = (p2 `2) - (o `2) by A9;

set r = (p2 `2) - (o `2);

consider g being Real such that

A30: 0 < g and

A31: ].(((p2 `2) - (o `2)) - g),(((p2 `2) - (o `2)) + g).[ c= V1 by A26, A29, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset of (TOP-REAL 2) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

take [:([#] (TOP-REAL 2)),W2:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )

A32: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A30, XREAL_1:6, XREAL_1:15;

then p2 in W2 by A32;

hence p in [:([#] (TOP-REAL 2)),W2:] by A28, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )

W2 is open by PSCOMP_1:21;

hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; :: thesis: Yo .: [:([#] (TOP-REAL 2)),W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Yo .: [:([#] (TOP-REAL 2)),W2:] or b in V )

assume b in Yo .: [:([#] (TOP-REAL 2)),W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A33: a in [:([#] (TOP-REAL 2)),W2:] and

A34: Yo . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A35: a = [a1,a2] and

A36: yo . a = (a2 `2) - (o `2) by A9;

a2 in W2 by A33, A35, ZFMISC_1:87;

then consider x2, y2 being Real such that

A37: a2 = |[x2,y2]| and

A38: ( (p2 `2) - g < y2 & y2 < (p2 `2) + g ) ;

a2 `2 = y2 by A37, EUCLID:52;

then ( ((p2 `2) - g) - (o `2) < (a2 `2) - (o `2) & (a2 `2) - (o `2) < ((p2 `2) + g) - (o `2) ) by A38, XREAL_1:9;

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 A31, A34, A36; :: thesis: verum

then reconsider yo = yo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

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

then
Xo is continuous
by JGRAPH_2:10;
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( Xo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Xo .: W c= V ) )

assume that

A39: Xo . p in V and

A40: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Xo .: W c= V )

reconsider V1 = V as open Subset of REAL by A40, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A41: p = [p1,p2] and

A42: Xo . p = (p2 `1) - (o `1) by A3;

set r = (p2 `1) - (o `1);

consider g being Real such that

A43: 0 < g and

A44: ].(((p2 `1) - (o `1)) - g),(((p2 `1) - (o `1)) + g).[ c= V1 by A39, A42, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2)

take [:([#] (TOP-REAL 2)),W2:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )

A45: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A43, XREAL_1:6, XREAL_1:15;

then p2 in W2 by A45;

hence p in [:([#] (TOP-REAL 2)),W2:] by A41, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )

W2 is open by PSCOMP_1:19;

hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; :: thesis: Xo .: [:([#] (TOP-REAL 2)),W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Xo .: [:([#] (TOP-REAL 2)),W2:] or b in V )

assume b in Xo .: [:([#] (TOP-REAL 2)),W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A46: a in [:([#] (TOP-REAL 2)),W2:] and

A47: Xo . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A48: a = [a1,a2] and

A49: xo . a = (a2 `1) - (o `1) by A3;

a2 in W2 by A46, A48, ZFMISC_1:87;

then consider x2, y2 being Real such that

A50: a2 = |[x2,y2]| and

A51: ( (p2 `1) - g < x2 & x2 < (p2 `1) + g ) ;

a2 `1 = x2 by A50, EUCLID:52;

then ( ((p2 `1) - g) - (o `1) < (a2 `1) - (o `1) & (a2 `1) - (o `1) < ((p2 `1) + g) - (o `1) ) by A51, XREAL_1:9;

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 A44, A47, A49; :: thesis: verum

end;ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Xo .: W c= V )

let V be Subset of R^1; :: thesis: ( Xo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Xo .: W c= V ) )

assume that

A39: Xo . p in V and

A40: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Xo .: W c= V )

reconsider V1 = V as open Subset of REAL by A40, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A41: p = [p1,p2] and

A42: Xo . p = (p2 `1) - (o `1) by A3;

set r = (p2 `1) - (o `1);

consider g being Real such that

A43: 0 < g and

A44: ].(((p2 `1) - (o `1)) - g),(((p2 `1) - (o `1)) + g).[ c= V1 by A39, A42, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset of (TOP-REAL 2) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

take [:([#] (TOP-REAL 2)),W2:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )

A45: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A43, XREAL_1:6, XREAL_1:15;

then p2 in W2 by A45;

hence p in [:([#] (TOP-REAL 2)),W2:] by A41, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )

W2 is open by PSCOMP_1:19;

hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; :: thesis: Xo .: [:([#] (TOP-REAL 2)),W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Xo .: [:([#] (TOP-REAL 2)),W2:] or b in V )

assume b in Xo .: [:([#] (TOP-REAL 2)),W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A46: a in [:([#] (TOP-REAL 2)),W2:] and

A47: Xo . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A48: a = [a1,a2] and

A49: xo . a = (a2 `1) - (o `1) by A3;

a2 in W2 by A46, A48, ZFMISC_1:87;

then consider x2, y2 being Real such that

A50: a2 = |[x2,y2]| and

A51: ( (p2 `1) - g < x2 & x2 < (p2 `1) + g ) ;

a2 `1 = x2 by A50, EUCLID:52;

then ( ((p2 `1) - g) - (o `1) < (a2 `1) - (o `1) & (a2 `1) - (o `1) < ((p2 `1) + g) - (o `1) ) by A51, XREAL_1:9;

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 A44, A47, A49; :: thesis: verum

then reconsider xo = xo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

set Zyo = yo | OK;

set Zxo = xo | OK;

set p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK);

set g = BR-map f;

A52: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) = OK by PRE_TOPC:8;

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

then
Dy is continuous
by JGRAPH_2:10;
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( Dy . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dy .: W c= V ) )

assume that

A53: Dy . p in V and

A54: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dy .: W c= V )

reconsider V1 = V as open Subset of REAL by A54, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A55: p = [p1,p2] and

A56: dy . p = (p1 `2) - (p2 `2) by A19;

set r = (p1 `2) - (p2 `2);

consider g being Real such that

A57: 0 < g and

A58: ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ c= V1 by A53, A56, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ;

A59: { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) by A59;

A61: 0 / 2 < g / 2 by A57, XREAL_1:74;

then ( (p2 `2) - (g / 2) < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + (g / 2) ) by XREAL_1:6, XREAL_1:15;

then A62: p2 in W2 by A60;

set W1 = { |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ;

{ |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

take [:W1,W2:] ; :: thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )

A63: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;

( (p1 `2) - (g / 2) < (p1 `2) - 0 & (p1 `2) + 0 < (p1 `2) + (g / 2) ) by A61, XREAL_1:6, XREAL_1:15;

then p1 in W1 by A63;

hence p in [:W1,W2:] by A55, A62, ZFMISC_1:def 2; :: thesis: ( [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )

( W1 is open & W2 is open ) by PSCOMP_1:21;

hence [:W1,W2:] is open by BORSUK_1:6; :: thesis: Dy .: [:W1,W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Dy .: [:W1,W2:] or b in V )

assume b in Dy .: [:W1,W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A64: a in [:W1,W2:] and

A65: Dy . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A66: a = [a1,a2] and

A67: dy . a = (a1 `2) - (a2 `2) by A19;

a2 in W2 by A64, A66, ZFMISC_1:87;

then consider x2, y2 being Real such that

A68: a2 = |[x2,y2]| and

A69: (p2 `2) - (g / 2) < y2 and

A70: y2 < (p2 `2) + (g / 2) ;

A71: a2 `2 = y2 by A68, EUCLID:52;

(p2 `2) - y2 > (p2 `2) - ((p2 `2) + (g / 2)) by A70, XREAL_1:15;

then A72: (p2 `2) - y2 > - (g / 2) ;

((p2 `2) - (g / 2)) + (g / 2) < y2 + (g / 2) by A69, XREAL_1:6;

then (p2 `2) - y2 < (y2 + (g / 2)) - y2 by XREAL_1:9;

then A73: |.((p2 `2) - y2).| < g / 2 by A72, SEQ_2:1;

a1 in W1 by A64, A66, ZFMISC_1:87;

then consider x1, y1 being Real such that

A74: a1 = |[x1,y1]| and

A75: (p1 `2) - (g / 2) < y1 and

A76: y1 < (p1 `2) + (g / 2) ;

(p1 `2) - y1 > (p1 `2) - ((p1 `2) + (g / 2)) by A76, XREAL_1:15;

then A77: (p1 `2) - y1 > - (g / 2) ;

|.(((p1 `2) - y1) - ((p2 `2) - y2)).| <= |.((p1 `2) - y1).| + |.((p2 `2) - y2).| by COMPLEX1:57;

then A78: |.(- (((p1 `2) - y1) - ((p2 `2) - y2))).| <= |.((p1 `2) - y1).| + |.((p2 `2) - y2).| by COMPLEX1:52;

((p1 `2) - (g / 2)) + (g / 2) < y1 + (g / 2) by A75, XREAL_1:6;

then (p1 `2) - y1 < (y1 + (g / 2)) - y1 by XREAL_1:9;

then |.((p1 `2) - y1).| < g / 2 by A77, SEQ_2:1;

then |.((p1 `2) - y1).| + |.((p2 `2) - y2).| < (g / 2) + (g / 2) by A73, XREAL_1:8;

then A79: |.((y1 - y2) - ((p1 `2) - (p2 `2))).| < g by A78, XXREAL_0:2;

a1 `2 = y1 by A74, EUCLID:52;

then (a1 `2) - (a2 `2) in ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ by A71, A79, RCOMP_1:1;

hence b in V by A58, A65, A67; :: thesis: verum

end;ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dy .: W c= V )

let V be Subset of R^1; :: thesis: ( Dy . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dy .: W c= V ) )

assume that

A53: Dy . p in V and

A54: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dy .: W c= V )

reconsider V1 = V as open Subset of REAL by A54, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A55: p = [p1,p2] and

A56: dy . p = (p1 `2) - (p2 `2) by A19;

set r = (p1 `2) - (p2 `2);

consider g being Real such that

A57: 0 < g and

A58: ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ c= V1 by A53, A56, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ;

A59: { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

A60:
p2 = |[(p2 `1),(p2 `2)]|
by EUCLID:53;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) by A59;

A61: 0 / 2 < g / 2 by A57, XREAL_1:74;

then ( (p2 `2) - (g / 2) < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + (g / 2) ) by XREAL_1:6, XREAL_1:15;

then A62: p2 in W2 by A60;

set W1 = { |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ;

{ |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider W1 = { |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

take [:W1,W2:] ; :: thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )

A63: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;

( (p1 `2) - (g / 2) < (p1 `2) - 0 & (p1 `2) + 0 < (p1 `2) + (g / 2) ) by A61, XREAL_1:6, XREAL_1:15;

then p1 in W1 by A63;

hence p in [:W1,W2:] by A55, A62, ZFMISC_1:def 2; :: thesis: ( [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )

( W1 is open & W2 is open ) by PSCOMP_1:21;

hence [:W1,W2:] is open by BORSUK_1:6; :: thesis: Dy .: [:W1,W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Dy .: [:W1,W2:] or b in V )

assume b in Dy .: [:W1,W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A64: a in [:W1,W2:] and

A65: Dy . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A66: a = [a1,a2] and

A67: dy . a = (a1 `2) - (a2 `2) by A19;

a2 in W2 by A64, A66, ZFMISC_1:87;

then consider x2, y2 being Real such that

A68: a2 = |[x2,y2]| and

A69: (p2 `2) - (g / 2) < y2 and

A70: y2 < (p2 `2) + (g / 2) ;

A71: a2 `2 = y2 by A68, EUCLID:52;

(p2 `2) - y2 > (p2 `2) - ((p2 `2) + (g / 2)) by A70, XREAL_1:15;

then A72: (p2 `2) - y2 > - (g / 2) ;

((p2 `2) - (g / 2)) + (g / 2) < y2 + (g / 2) by A69, XREAL_1:6;

then (p2 `2) - y2 < (y2 + (g / 2)) - y2 by XREAL_1:9;

then A73: |.((p2 `2) - y2).| < g / 2 by A72, SEQ_2:1;

a1 in W1 by A64, A66, ZFMISC_1:87;

then consider x1, y1 being Real such that

A74: a1 = |[x1,y1]| and

A75: (p1 `2) - (g / 2) < y1 and

A76: y1 < (p1 `2) + (g / 2) ;

(p1 `2) - y1 > (p1 `2) - ((p1 `2) + (g / 2)) by A76, XREAL_1:15;

then A77: (p1 `2) - y1 > - (g / 2) ;

|.(((p1 `2) - y1) - ((p2 `2) - y2)).| <= |.((p1 `2) - y1).| + |.((p2 `2) - y2).| by COMPLEX1:57;

then A78: |.(- (((p1 `2) - y1) - ((p2 `2) - y2))).| <= |.((p1 `2) - y1).| + |.((p2 `2) - y2).| by COMPLEX1:52;

((p1 `2) - (g / 2)) + (g / 2) < y1 + (g / 2) by A75, XREAL_1:6;

then (p1 `2) - y1 < (y1 + (g / 2)) - y1 by XREAL_1:9;

then |.((p1 `2) - y1).| < g / 2 by A77, SEQ_2:1;

then |.((p1 `2) - y1).| + |.((p2 `2) - y2).| < (g / 2) + (g / 2) by A73, XREAL_1:8;

then A79: |.((y1 - y2) - ((p1 `2) - (p2 `2))).| < g by A78, XXREAL_0:2;

a1 `2 = y1 by A74, EUCLID:52;

then (a1 `2) - (a2 `2) in ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ by A71, A79, RCOMP_1:1;

hence b in V by A58, A65, A67; :: thesis: verum

then reconsider dy = dy as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

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

then
Dx is continuous
by JGRAPH_2:10;
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( Dx . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dx .: W c= V ) )

assume that

A80: Dx . p in V and

A81: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dx .: W c= V )

reconsider V1 = V as open Subset of REAL by A81, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A82: p = [p1,p2] and

A83: dx . p = (p1 `1) - (p2 `1) by A25;

set r = (p1 `1) - (p2 `1);

consider g being Real such that

A84: 0 < g and

A85: ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ c= V1 by A80, A83, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ;

A86: { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) by A86;

A88: 0 / 2 < g / 2 by A84, XREAL_1:74;

then ( (p2 `1) - (g / 2) < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + (g / 2) ) by XREAL_1:6, XREAL_1:15;

then A89: p2 in W2 by A87;

set W1 = { |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ;

{ |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

take [:W1,W2:] ; :: thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )

A90: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;

( (p1 `1) - (g / 2) < (p1 `1) - 0 & (p1 `1) + 0 < (p1 `1) + (g / 2) ) by A88, XREAL_1:6, XREAL_1:15;

then p1 in W1 by A90;

hence p in [:W1,W2:] by A82, A89, ZFMISC_1:def 2; :: thesis: ( [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )

( W1 is open & W2 is open ) by PSCOMP_1:19;

hence [:W1,W2:] is open by BORSUK_1:6; :: thesis: Dx .: [:W1,W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Dx .: [:W1,W2:] or b in V )

assume b in Dx .: [:W1,W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A91: a in [:W1,W2:] and

A92: Dx . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A93: a = [a1,a2] and

A94: dx . a = (a1 `1) - (a2 `1) by A25;

a2 in W2 by A91, A93, ZFMISC_1:87;

then consider x2, y2 being Real such that

A95: a2 = |[x2,y2]| and

A96: (p2 `1) - (g / 2) < x2 and

A97: x2 < (p2 `1) + (g / 2) ;

A98: a2 `1 = x2 by A95, EUCLID:52;

(p2 `1) - x2 > (p2 `1) - ((p2 `1) + (g / 2)) by A97, XREAL_1:15;

then A99: (p2 `1) - x2 > - (g / 2) ;

((p2 `1) - (g / 2)) + (g / 2) < x2 + (g / 2) by A96, XREAL_1:6;

then (p2 `1) - x2 < (x2 + (g / 2)) - x2 by XREAL_1:9;

then A100: |.((p2 `1) - x2).| < g / 2 by A99, SEQ_2:1;

a1 in W1 by A91, A93, ZFMISC_1:87;

then consider x1, y1 being Real such that

A101: a1 = |[x1,y1]| and

A102: (p1 `1) - (g / 2) < x1 and

A103: x1 < (p1 `1) + (g / 2) ;

(p1 `1) - x1 > (p1 `1) - ((p1 `1) + (g / 2)) by A103, XREAL_1:15;

then A104: (p1 `1) - x1 > - (g / 2) ;

|.(((p1 `1) - x1) - ((p2 `1) - x2)).| <= |.((p1 `1) - x1).| + |.((p2 `1) - x2).| by COMPLEX1:57;

then A105: |.(- (((p1 `1) - x1) - ((p2 `1) - x2))).| <= |.((p1 `1) - x1).| + |.((p2 `1) - x2).| by COMPLEX1:52;

((p1 `1) - (g / 2)) + (g / 2) < x1 + (g / 2) by A102, XREAL_1:6;

then (p1 `1) - x1 < (x1 + (g / 2)) - x1 by XREAL_1:9;

then |.((p1 `1) - x1).| < g / 2 by A104, SEQ_2:1;

then |.((p1 `1) - x1).| + |.((p2 `1) - x2).| < (g / 2) + (g / 2) by A100, XREAL_1:8;

then A106: |.((x1 - x2) - ((p1 `1) - (p2 `1))).| < g by A105, XXREAL_0:2;

a1 `1 = x1 by A101, EUCLID:52;

then (a1 `1) - (a2 `1) in ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ by A98, A106, RCOMP_1:1;

hence b in V by A85, A92, A94; :: thesis: verum

end;ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dx .: W c= V )

let V be Subset of R^1; :: thesis: ( Dx . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dx .: W c= V ) )

assume that

A80: Dx . p in V and

A81: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & Dx .: W c= V )

reconsider V1 = V as open Subset of REAL by A81, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A82: p = [p1,p2] and

A83: dx . p = (p1 `1) - (p2 `1) by A25;

set r = (p1 `1) - (p2 `1);

consider g being Real such that

A84: 0 < g and

A85: ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ c= V1 by A80, A83, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ;

A86: { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

A87:
p2 = |[(p2 `1),(p2 `2)]|
by EUCLID:53;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) by A86;

A88: 0 / 2 < g / 2 by A84, XREAL_1:74;

then ( (p2 `1) - (g / 2) < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + (g / 2) ) by XREAL_1:6, XREAL_1:15;

then A89: p2 in W2 by A87;

set W1 = { |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ;

{ |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider W1 = { |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being 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: verum

take [:W1,W2:] ; :: thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )

A90: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;

( (p1 `1) - (g / 2) < (p1 `1) - 0 & (p1 `1) + 0 < (p1 `1) + (g / 2) ) by A88, XREAL_1:6, XREAL_1:15;

then p1 in W1 by A90;

hence p in [:W1,W2:] by A82, A89, ZFMISC_1:def 2; :: thesis: ( [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )

( W1 is open & W2 is open ) by PSCOMP_1:19;

hence [:W1,W2:] is open by BORSUK_1:6; :: thesis: Dx .: [:W1,W2:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Dx .: [:W1,W2:] or b in V )

assume b in Dx .: [:W1,W2:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A91: a in [:W1,W2:] and

A92: Dx . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A93: a = [a1,a2] and

A94: dx . a = (a1 `1) - (a2 `1) by A25;

a2 in W2 by A91, A93, ZFMISC_1:87;

then consider x2, y2 being Real such that

A95: a2 = |[x2,y2]| and

A96: (p2 `1) - (g / 2) < x2 and

A97: x2 < (p2 `1) + (g / 2) ;

A98: a2 `1 = x2 by A95, EUCLID:52;

(p2 `1) - x2 > (p2 `1) - ((p2 `1) + (g / 2)) by A97, XREAL_1:15;

then A99: (p2 `1) - x2 > - (g / 2) ;

((p2 `1) - (g / 2)) + (g / 2) < x2 + (g / 2) by A96, XREAL_1:6;

then (p2 `1) - x2 < (x2 + (g / 2)) - x2 by XREAL_1:9;

then A100: |.((p2 `1) - x2).| < g / 2 by A99, SEQ_2:1;

a1 in W1 by A91, A93, ZFMISC_1:87;

then consider x1, y1 being Real such that

A101: a1 = |[x1,y1]| and

A102: (p1 `1) - (g / 2) < x1 and

A103: x1 < (p1 `1) + (g / 2) ;

(p1 `1) - x1 > (p1 `1) - ((p1 `1) + (g / 2)) by A103, XREAL_1:15;

then A104: (p1 `1) - x1 > - (g / 2) ;

|.(((p1 `1) - x1) - ((p2 `1) - x2)).| <= |.((p1 `1) - x1).| + |.((p2 `1) - x2).| by COMPLEX1:57;

then A105: |.(- (((p1 `1) - x1) - ((p2 `1) - x2))).| <= |.((p1 `1) - x1).| + |.((p2 `1) - x2).| by COMPLEX1:52;

((p1 `1) - (g / 2)) + (g / 2) < x1 + (g / 2) by A102, XREAL_1:6;

then (p1 `1) - x1 < (x1 + (g / 2)) - x1 by XREAL_1:9;

then |.((p1 `1) - x1).| < g / 2 by A104, SEQ_2:1;

then |.((p1 `1) - x1).| + |.((p2 `1) - x2).| < (g / 2) + (g / 2) by A100, XREAL_1:8;

then A106: |.((x1 - x2) - ((p1 `1) - (p2 `1))).| < g by A105, XXREAL_0:2;

a1 `1 = x1 by A101, EUCLID:52;

then (a1 `1) - (a2 `1) in ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ by A98, A106, RCOMP_1:1;

hence b in V by A85, A92, A94; :: thesis: verum

then reconsider dx = dx as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

set Zdy = dy | OK;

set Zdx = dx | OK;

set m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK));

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

then
fY2 is continuous
by JGRAPH_2:10;
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( fY2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fY2 .: W c= V ) )

assume that

A107: fY2 . p in V and

A108: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fY2 .: W c= V )

reconsider V1 = V as open Subset of REAL by A108, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A109: p = [p1,p2] and

A110: fY2 . p = p2 `2 by A22;

consider g being Real such that

A111: 0 < g and

A112: ].((p2 `2) - g),((p2 `2) + g).[ c= V1 by A107, A110, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W1 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2)

take [:([#] (TOP-REAL 2)),W1:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

A113: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A111, XREAL_1:6, XREAL_1:15;

then p2 in W1 by A113;

hence p in [:([#] (TOP-REAL 2)),W1:] by A109, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

W1 is open by PSCOMP_1:21;

hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; :: thesis: fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in fY2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )

assume b in fY2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A114: a in [:([#] (TOP-REAL 2)),W1:] and

A115: fY2 . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A116: a = [a1,a2] and

A117: fY2 . a = a2 `2 by A22;

a2 in W1 by A114, A116, ZFMISC_1:87;

then consider x1, y1 being Real such that

A118: a2 = |[x1,y1]| and

A119: (p2 `2) - g < y1 and

A120: y1 < (p2 `2) + g ;

(p2 `2) - y1 > (p2 `2) - ((p2 `2) + g) by A120, XREAL_1:15;

then A121: (p2 `2) - y1 > - g ;

((p2 `2) - g) + g < y1 + g by A119, XREAL_1:6;

then (p2 `2) - y1 < (y1 + g) - y1 by XREAL_1:9;

then |.((p2 `2) - y1).| < g by A121, SEQ_2:1;

then |.(- ((p2 `2) - y1)).| < g by COMPLEX1:52;

then A122: |.(y1 - (p2 `2)).| < g ;

a2 `2 = y1 by A118, EUCLID:52;

then a2 `2 in ].((p2 `2) - g),((p2 `2) + g).[ by A122, RCOMP_1:1;

hence b in V by A112, A115, A117; :: thesis: verum

end;ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fY2 .: W c= V )

let V be Subset of R^1; :: thesis: ( fY2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fY2 .: W c= V ) )

assume that

A107: fY2 . p in V and

A108: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fY2 .: W c= V )

reconsider V1 = V as open Subset of REAL by A108, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A109: p = [p1,p2] and

A110: fY2 . p = p2 `2 by A22;

consider g being Real such that

A111: 0 < g and

A112: ].((p2 `2) - g),((p2 `2) + g).[ c= V1 by A107, A110, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W1 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider W1 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset of (TOP-REAL 2) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

take [:([#] (TOP-REAL 2)),W1:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

A113: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A111, XREAL_1:6, XREAL_1:15;

then p2 in W1 by A113;

hence p in [:([#] (TOP-REAL 2)),W1:] by A109, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

W1 is open by PSCOMP_1:21;

hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; :: thesis: fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in fY2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )

assume b in fY2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A114: a in [:([#] (TOP-REAL 2)),W1:] and

A115: fY2 . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A116: a = [a1,a2] and

A117: fY2 . a = a2 `2 by A22;

a2 in W1 by A114, A116, ZFMISC_1:87;

then consider x1, y1 being Real such that

A118: a2 = |[x1,y1]| and

A119: (p2 `2) - g < y1 and

A120: y1 < (p2 `2) + g ;

(p2 `2) - y1 > (p2 `2) - ((p2 `2) + g) by A120, XREAL_1:15;

then A121: (p2 `2) - y1 > - g ;

((p2 `2) - g) + g < y1 + g by A119, XREAL_1:6;

then (p2 `2) - y1 < (y1 + g) - y1 by XREAL_1:9;

then |.((p2 `2) - y1).| < g by A121, SEQ_2:1;

then |.(- ((p2 `2) - y1)).| < g by COMPLEX1:52;

then A122: |.(y1 - (p2 `2)).| < g ;

a2 `2 = y1 by A118, EUCLID:52;

then a2 `2 in ].((p2 `2) - g),((p2 `2) + g).[ by A122, RCOMP_1:1;

hence b in V by A112, A115, A117; :: thesis: verum

then reconsider fy2 = fy2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

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

then
fX2 is continuous
by JGRAPH_2:10;
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: 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 )

let V be Subset of R^1; :: thesis: ( fX2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fX2 .: W c= V ) )

assume that

A123: fX2 . p in V and

A124: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fX2 .: W c= V )

reconsider V1 = V as open Subset of REAL by A124, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A125: p = [p1,p2] and

A126: fX2 . p = p2 `1 by A6;

consider g being Real such that

A127: 0 < g and

A128: ].((p2 `1) - g),((p2 `1) + g).[ c= V1 by A123, A126, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W1 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2)

take [:([#] (TOP-REAL 2)),W1:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

A129: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A127, XREAL_1:6, XREAL_1:15;

then p2 in W1 by A129;

hence p in [:([#] (TOP-REAL 2)),W1:] by A125, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

W1 is open by PSCOMP_1:19;

hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; :: thesis: fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in fX2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )

assume b in fX2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A130: a in [:([#] (TOP-REAL 2)),W1:] and

A131: fX2 . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A132: a = [a1,a2] and

A133: fX2 . a = a2 `1 by A6;

a2 in W1 by A130, A132, ZFMISC_1:87;

then consider x1, y1 being Real such that

A134: a2 = |[x1,y1]| and

A135: (p2 `1) - g < x1 and

A136: x1 < (p2 `1) + g ;

(p2 `1) - x1 > (p2 `1) - ((p2 `1) + g) by A136, XREAL_1:15;

then A137: (p2 `1) - x1 > - g ;

((p2 `1) - g) + g < x1 + g by A135, XREAL_1:6;

then (p2 `1) - x1 < (x1 + g) - x1 by XREAL_1:9;

then |.((p2 `1) - x1).| < g by A137, SEQ_2:1;

then |.(- ((p2 `1) - x1)).| < g by COMPLEX1:52;

then A138: |.(x1 - (p2 `1)).| < g ;

a2 `1 = x1 by A134, EUCLID:52;

then a2 `1 in ].((p2 `1) - g),((p2 `1) + g).[ by A138, RCOMP_1:1;

hence b in V by A128, A131, A133; :: thesis: verum

end;ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fX2 .: W c= V )

let V be Subset of R^1; :: thesis: ( fX2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fX2 .: W c= V ) )

assume that

A123: fX2 . p in V and

A124: V is open ; :: thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st

( p in W & W is open & fX2 .: W c= V )

reconsider V1 = V as open Subset of REAL by A124, BORSUK_5:39, TOPMETR:17;

consider p1, p2 being Point of (TOP-REAL 2) such that

A125: p = [p1,p2] and

A126: fX2 . p = p2 `1 by A6;

consider g being Real such that

A127: 0 < g and

A128: ].((p2 `1) - g),((p2 `1) + g).[ c= V1 by A123, A126, RCOMP_1:19;

reconsider g = g as Element of REAL by XREAL_0:def 1;

set W1 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ;

{ |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2)

proof

then reconsider W1 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset of (TOP-REAL 2) ;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } or a in the carrier of (TOP-REAL 2) )

assume a in { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

end;assume a in { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; :: thesis: a in the carrier of (TOP-REAL 2)

then ex x, y being Real st

( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ;

hence a in the carrier of (TOP-REAL 2) ; :: thesis: verum

take [:([#] (TOP-REAL 2)),W1:] ; :: thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

A129: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;

( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A127, XREAL_1:6, XREAL_1:15;

then p2 in W1 by A129;

hence p in [:([#] (TOP-REAL 2)),W1:] by A125, ZFMISC_1:def 2; :: thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )

W1 is open by PSCOMP_1:19;

hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; :: thesis: fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in fX2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )

assume b in fX2 .: [:([#] (TOP-REAL 2)),W1:] ; :: thesis: b in V

then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that

A130: a in [:([#] (TOP-REAL 2)),W1:] and

A131: fX2 . a = b by FUNCT_2:65;

consider a1, a2 being Point of (TOP-REAL 2) such that

A132: a = [a1,a2] and

A133: fX2 . a = a2 `1 by A6;

a2 in W1 by A130, A132, ZFMISC_1:87;

then consider x1, y1 being Real such that

A134: a2 = |[x1,y1]| and

A135: (p2 `1) - g < x1 and

A136: x1 < (p2 `1) + g ;

(p2 `1) - x1 > (p2 `1) - ((p2 `1) + g) by A136, XREAL_1:15;

then A137: (p2 `1) - x1 > - g ;

((p2 `1) - g) + g < x1 + g by A135, XREAL_1:6;

then (p2 `1) - x1 < (x1 + g) - x1 by XREAL_1:9;

then |.((p2 `1) - x1).| < g by A137, SEQ_2:1;

then |.(- ((p2 `1) - x1)).| < g by COMPLEX1:52;

then A138: |.(x1 - (p2 `1)).| < g ;

a2 `1 = x1 by A134, EUCLID:52;

then a2 `1 in ].((p2 `1) - g),((p2 `1) + g).[ by A138, RCOMP_1:1;

hence b in V by A128, A131, A133; :: thesis: verum

then reconsider fx2 = fx2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;

set yy = (yo | OK) (#) (dy | OK);

set xx = (xo | OK) (#) (dx | OK);

set Zfy2 = fy2 | OK;

set Zfx2 = fx2 | OK;

set p1 = (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)));

A139: dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def 1;

A140: 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: ( y <> z implies [y,z] in OK )

A141: ( y is Point of (TOP-REAL 2) & z is Point of (TOP-REAL 2) ) by PRE_TOPC:25;

assume y <> z ; :: thesis: [y,z] in OK

then [y,z] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A141;

hence [y,z] in OK by XBOOLE_0:def 4; :: thesis: verum

end;A141: ( y is Point of (TOP-REAL 2) & z is Point of (TOP-REAL 2) ) by PRE_TOPC:25;

assume y <> z ; :: thesis: [y,z] in OK

then [y,z] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A141;

hence [y,z] in OK by XBOOLE_0:def 4; :: thesis: verum

A142: now :: thesis: for b being Real st b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) holds

0 >= b

0 >= b

let b be Real; :: thesis: ( b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) implies 0 >= b )

assume b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) ; :: thesis: 0 >= b

then consider a being object such that

A143: a in dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) and

A144: ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . a = b by FUNCT_1:def 3;

a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A143, XBOOLE_0:def 4;

then consider y, z being Point of (TOP-REAL 2) such that

A145: a = [y,z] and

A146: y <> z ;

a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A143, XBOOLE_0:def 4;

then consider a1, a2 being Point of (Tdisk (o,r)) such that

A147: a = [a1,a2] by BORSUK_1:10;

A148: a2 = z by A145, A147, XTUPLE_0:1;

A149: a1 = y by A145, A147, XTUPLE_0:1;

then A150: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A146, A148, FUNCT_1:49;

set r3 = (z `1) - (o `1);

set r4 = (z `2) - (o `2);

consider x9, x10 being Point of (TOP-REAL 2) such that

A151: [y,z] = [x9,x10] and

A152: xo . [y,z] = (x10 `1) - (o `1) by A3;

A153: z = x10 by A151, XTUPLE_0:1;

the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;

then |.(z - o).| <= r by A148, TOPREAL9:8;

then A154: |.(z - o).| ^2 <= r ^2 by SQUARE_1:15;

consider x11, x12 being Point of (TOP-REAL 2) such that

A155: [y,z] = [x11,x12] and

A156: yo . [y,z] = (x12 `2) - (o `2) by A9;

A157: z = x12 by A155, XTUPLE_0:1;

A158: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A146, A149, A148, FUNCT_1:49;

|.(z - o).| ^2 = (((z - o) `1) ^2) + (((z - o) `2) ^2) by JGRAPH_1:29

.= (((z `1) - (o `1)) ^2) + (((z - o) `2) ^2) by TOPREAL3:3

.= (((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2) by TOPREAL3:3 ;

then A159: ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) <= (r ^2) - (r ^2) by A154, XREAL_1:9;

A160: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A143, A145, PRE_TOPC:def 5;

((((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 A143, A145, VALUED_1:13

.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A150, FUNCOP_1:7

.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A160, 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 A158, A152, A153, A156, A157, VALUED_1:5 ;

hence 0 >= b by A144, A145, A159; :: thesis: verum

end;assume b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) ; :: thesis: 0 >= b

then consider a being object such that

A143: a in dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) and

A144: ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . a = b by FUNCT_1:def 3;

a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A143, XBOOLE_0:def 4;

then consider y, z being Point of (TOP-REAL 2) such that

A145: a = [y,z] and

A146: y <> z ;

a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A143, XBOOLE_0:def 4;

then consider a1, a2 being Point of (Tdisk (o,r)) such that

A147: a = [a1,a2] by BORSUK_1:10;

A148: a2 = z by A145, A147, XTUPLE_0:1;

A149: a1 = y by A145, A147, XTUPLE_0:1;

then A150: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A146, A148, FUNCT_1:49;

set r3 = (z `1) - (o `1);

set r4 = (z `2) - (o `2);

consider x9, x10 being Point of (TOP-REAL 2) such that

A151: [y,z] = [x9,x10] and

A152: xo . [y,z] = (x10 `1) - (o `1) by A3;

A153: z = x10 by A151, XTUPLE_0:1;

the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;

then |.(z - o).| <= r by A148, TOPREAL9:8;

then A154: |.(z - o).| ^2 <= r ^2 by SQUARE_1:15;

consider x11, x12 being Point of (TOP-REAL 2) such that

A155: [y,z] = [x11,x12] and

A156: yo . [y,z] = (x12 `2) - (o `2) by A9;

A157: z = x12 by A155, XTUPLE_0:1;

A158: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A146, A149, A148, FUNCT_1:49;

|.(z - o).| ^2 = (((z - o) `1) ^2) + (((z - o) `2) ^2) by JGRAPH_1:29

.= (((z `1) - (o `1)) ^2) + (((z - o) `2) ^2) by TOPREAL3:3

.= (((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2) by TOPREAL3:3 ;

then A159: ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) <= (r ^2) - (r ^2) by A154, XREAL_1:9;

A160: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A143, A145, PRE_TOPC:def 5;

((((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 A143, A145, VALUED_1:13

.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A150, FUNCOP_1:7

.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A160, 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 A158, A152, A153, A156, A157, VALUED_1:5 ;

hence 0 >= b by A144, A145, A159; :: thesis: verum

now :: thesis: for b being Real st b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) holds

0 < b

then reconsider m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK)) as positive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by PARTFUN3:def 1;0 < b

let b be Real; :: thesis: ( b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) implies 0 < b )

assume b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) ; :: thesis: 0 < b

then consider a being object such that

A161: a in dom (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) and

A162: (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . a = b by FUNCT_1:def 3;

a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A161, XBOOLE_0:def 4;

then consider y, z being Point of (TOP-REAL 2) such that

A163: a = [y,z] and

A164: y <> z ;

a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A161, XBOOLE_0:def 4;

then consider a1, a2 being Point of (Tdisk (o,r)) such that

A165: a = [a1,a2] by BORSUK_1:10;

set r1 = (y `1) - (z `1);

set r2 = (y `2) - (z `2);

A167: [y,z] = [x3,x4] and

A168: dx . [y,z] = (x3 `1) - (x4 `1) by A25;

A169: ( y = x3 & z = x4 ) by A167, XTUPLE_0:1;

( a1 = y & a2 = z ) by A163, A165, XTUPLE_0:1;

then A170: ( (dx | OK) . [y,z] = dx . [y,z] & (dy | OK) . [y,z] = dy . [y,z] ) by A140, A164, FUNCT_1:49;

consider x5, x6 being Point of (TOP-REAL 2) such that

A171: [y,z] = [x5,x6] and

A172: dy . [y,z] = (x5 `2) - (x6 `2) by A19;

A173: ( y = x5 & z = x6 ) by A171, XTUPLE_0:1;

A174: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A161, A163, PRE_TOPC:def 5;

(((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A174, 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 A168, A169, A172, A173, A170, VALUED_1:5 ;

hence 0 < b by A162, A163, A166; :: thesis: verum

end;assume b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) ; :: thesis: 0 < b

then consider a being object such that

A161: a in dom (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) and

A162: (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . a = b by FUNCT_1:def 3;

a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A161, XBOOLE_0:def 4;

then consider y, z being Point of (TOP-REAL 2) such that

A163: a = [y,z] and

A164: y <> z ;

a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A161, XBOOLE_0:def 4;

then consider a1, a2 being Point of (Tdisk (o,r)) such that

A165: a = [a1,a2] by BORSUK_1:10;

set r1 = (y `1) - (z `1);

set r2 = (y `2) - (z `2);

A166: now :: thesis: not (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) = 0

consider x3, x4 being Point of (TOP-REAL 2) such that assume
(((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) = 0
; :: thesis: contradiction

then ( (y `1) - (z `1) = 0 & (y `2) - (z `2) = 0 ) by COMPLEX1:1;

hence contradiction by A164, TOPREAL3:6; :: thesis: verum

end;then ( (y `1) - (z `1) = 0 & (y `2) - (z `2) = 0 ) by COMPLEX1:1;

hence contradiction by A164, TOPREAL3:6; :: thesis: verum

A167: [y,z] = [x3,x4] and

A168: dx . [y,z] = (x3 `1) - (x4 `1) by A25;

A169: ( y = x3 & z = x4 ) by A167, XTUPLE_0:1;

( a1 = y & a2 = z ) by A163, A165, XTUPLE_0:1;

then A170: ( (dx | OK) . [y,z] = dx . [y,z] & (dy | OK) . [y,z] = dy . [y,z] ) by A140, A164, FUNCT_1:49;

consider x5, x6 being Point of (TOP-REAL 2) such that

A171: [y,z] = [x5,x6] and

A172: dy . [y,z] = (x5 `2) - (x6 `2) by A19;

A173: ( y = x5 & z = x6 ) by A171, XTUPLE_0:1;

A174: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A161, A163, PRE_TOPC:def 5;

(((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A174, 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 A168, A169, A172, A173, A170, VALUED_1:5 ;

hence 0 < b by A162, A163, A166; :: thesis: verum

reconsider p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK) as nonpositive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A142, PARTFUN3:def 3;

set pp = ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2);

set k = ((- (((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;

set x3 = (fx2 | OK) + ((((- (((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));

set y3 = (fy2 | OK) + ((((- (((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));

reconsider X3 = (fx2 | OK) + ((((- (((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)), Y3 = (fy2 | OK) + ((((- (((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)) as Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),R^1 by TOPMETR:17;

set F = <:X3,Y3:>;

A175: for x being Point of (Tdisk (o,r)) holds (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)]

proof

( X3 is continuous & Y3 is continuous )
by JORDAN5A:27;
A176:
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;

let x be Point of (Tdisk (o,r)); :: thesis: (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)]

A177: ( dom X3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom Y3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) ) by FUNCT_2:def 1;

A178: not x is_a_fixpoint_of f by A16;

then A179: x <> f . x ;

consider y, z being Point of (TOP-REAL 2) such that

A180: ( y = x & z = f . x ) and

A181: HC (x,f) = HC (z,y,o,r) by A178, Def4;

A182: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A180, A179, FUNCT_1:49;

A183: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A180, A179, FUNCT_1:49;

set r1 = (y `1) - (z `1);

set r2 = (y `2) - (z `2);

set r3 = (z `1) - (o `1);

set r4 = (z `2) - (o `2);

consider x9, x10 being Point of (TOP-REAL 2) such that

A184: [y,z] = [x9,x10] and

A185: xo . [y,z] = (x10 `1) - (o `1) by A3;

A186: z = x10 by A184, XTUPLE_0:1;

consider x11, x12 being Point of (TOP-REAL 2) such that

A187: [y,z] = [x11,x12] and

A188: yo . [y,z] = (x12 `2) - (o `2) by A9;

A189: z = x12 by A187, XTUPLE_0:1;

[x,(f . x)] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A180, A179;

then A190: [y,z] in OK by A180, XBOOLE_0:def 4;

then A191: p2 . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A52, A139, VALUED_1:13

.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A182, FUNCOP_1:7

.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A52, A190, 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 A185, A186, A188, A189, A183, VALUED_1:5 ;

A192: (dx | OK) . [y,z] = dx . [y,z] by A140, A180, A179, FUNCT_1:49;

consider x7, x8 being Point of (TOP-REAL 2) such that

A193: [y,z] = [x7,x8] and

A194: fy2 . [y,z] = x8 `2 by A22;

A195: z = x8 by A193, XTUPLE_0:1;

consider x1, x2 being Point of (TOP-REAL 2) such that

A196: [y,z] = [x1,x2] and

A197: fx2 . [y,z] = x2 `1 by A6;

A198: z = x2 by A196, XTUPLE_0:1;

consider x3, x4 being Point of (TOP-REAL 2) such that

A199: [y,z] = [x3,x4] and

A200: dx . [y,z] = (x3 `1) - (x4 `1) by A25;

A201: ( y = x3 & z = x4 ) by A199, XTUPLE_0:1;

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

A202: ( ((xo | OK) (#) (dx | OK)) . [y,z] = ((xo | OK) . [y,z]) * ((dx | OK) . [y,z]) & ((yo | OK) (#) (dy | OK)) . [y,z] = ((yo | OK) . [y,z]) * ((dy | OK) . [y,z]) ) by VALUED_1:5;

A203: (dy | OK) . [y,z] = dy . [y,z] by A140, A180, A179, FUNCT_1:49;

consider x5, x6 being Point of (TOP-REAL 2) such that

A204: [y,z] = [x5,x6] and

A205: dy . [y,z] = (x5 `2) - (x6 `2) by A19;

A206: ( y = x5 & z = x6 ) by A204, XTUPLE_0:1;

A207: m . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A52, A190, 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 A200, A201, A205, A206, A192, A203, VALUED_1:5 ;

A208: (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) . [y,z] = (((xo | OK) (#) (dx | OK)) . [y,z]) + (((yo | OK) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1;

then A209: ((((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 A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, 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 A210: (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 A52, A190, 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 A52, A190, A176, 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 A207, A209, A191, 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 A211: (((- (((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 A52, A190, RFUNCT_1:def 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)))) . [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 A52, A190, A207, 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 A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, A208, A210, VALUED_1:8 ;

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 A52, A190, 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 A140, A180, A179, A194, A195, FUNCT_1:49

.= (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 A205, A206, A203, A211, VALUED_1:5 ;

A213: 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 A52, A190, 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 A140, A180, A179, A197, A198, FUNCT_1:49

.= (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 A200, A201, A192, A211, 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 A180, A181, A179, Th8

.= R2Homeomorphism . [(X3 . [y,z]),(Y3 . [y,z])] by A213, A212, TOPREALA:def 2

.= R2Homeomorphism . (<:X3,Y3:> . [y,z]) by A52, A190, A177, FUNCT_3:49

.= (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] by A52, A180, A190, FUNCT_2:15 ; :: thesis: verum

end;let x be Point of (Tdisk (o,r)); :: thesis: (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)]

A177: ( dom X3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom Y3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) ) by FUNCT_2:def 1;

A178: not x is_a_fixpoint_of f by A16;

then A179: x <> f . x ;

consider y, z being Point of (TOP-REAL 2) such that

A180: ( y = x & z = f . x ) and

A181: HC (x,f) = HC (z,y,o,r) by A178, Def4;

A182: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A180, A179, FUNCT_1:49;

A183: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A180, A179, FUNCT_1:49;

set r1 = (y `1) - (z `1);

set r2 = (y `2) - (z `2);

set r3 = (z `1) - (o `1);

set r4 = (z `2) - (o `2);

consider x9, x10 being Point of (TOP-REAL 2) such that

A184: [y,z] = [x9,x10] and

A185: xo . [y,z] = (x10 `1) - (o `1) by A3;

A186: z = x10 by A184, XTUPLE_0:1;

consider x11, x12 being Point of (TOP-REAL 2) such that

A187: [y,z] = [x11,x12] and

A188: yo . [y,z] = (x12 `2) - (o `2) by A9;

A189: z = x12 by A187, XTUPLE_0:1;

[x,(f . x)] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A180, A179;

then A190: [y,z] in OK by A180, XBOOLE_0:def 4;

then A191: p2 . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A52, A139, VALUED_1:13

.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A182, FUNCOP_1:7

.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A52, A190, 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 A185, A186, A188, A189, A183, VALUED_1:5 ;

A192: (dx | OK) . [y,z] = dx . [y,z] by A140, A180, A179, FUNCT_1:49;

consider x7, x8 being Point of (TOP-REAL 2) such that

A193: [y,z] = [x7,x8] and

A194: fy2 . [y,z] = x8 `2 by A22;

A195: z = x8 by A193, XTUPLE_0:1;

consider x1, x2 being Point of (TOP-REAL 2) such that

A196: [y,z] = [x1,x2] and

A197: fx2 . [y,z] = x2 `1 by A6;

A198: z = x2 by A196, XTUPLE_0:1;

consider x3, x4 being Point of (TOP-REAL 2) such that

A199: [y,z] = [x3,x4] and

A200: dx . [y,z] = (x3 `1) - (x4 `1) by A25;

A201: ( y = x3 & z = x4 ) by A199, XTUPLE_0:1;

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

A202: ( ((xo | OK) (#) (dx | OK)) . [y,z] = ((xo | OK) . [y,z]) * ((dx | OK) . [y,z]) & ((yo | OK) (#) (dy | OK)) . [y,z] = ((yo | OK) . [y,z]) * ((dy | OK) . [y,z]) ) by VALUED_1:5;

A203: (dy | OK) . [y,z] = dy . [y,z] by A140, A180, A179, FUNCT_1:49;

consider x5, x6 being Point of (TOP-REAL 2) such that

A204: [y,z] = [x5,x6] and

A205: dy . [y,z] = (x5 `2) - (x6 `2) by A19;

A206: ( y = x5 & z = x6 ) by A204, XTUPLE_0:1;

A207: m . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A52, A190, 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 A200, A201, A205, A206, A192, A203, VALUED_1:5 ;

A208: (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) . [y,z] = (((xo | OK) (#) (dx | OK)) . [y,z]) + (((yo | OK) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1;

then A209: ((((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 A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, 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 A210: (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 A52, A190, 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 A52, A190, A176, 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 A207, A209, A191, 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 A211: (((- (((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 A52, A190, RFUNCT_1:def 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)))) . [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 A52, A190, A207, 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 A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, A208, A210, VALUED_1:8 ;

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 A52, A190, 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 A140, A180, A179, A194, A195, FUNCT_1:49

.= (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 A205, A206, A203, A211, VALUED_1:5 ;

A213: 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 A52, A190, 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 A140, A180, A179, A197, A198, FUNCT_1:49

.= (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 A200, A201, A192, A211, 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 A180, A181, A179, Th8

.= R2Homeomorphism . [(X3 . [y,z]),(Y3 . [y,z])] by A213, A212, TOPREALA:def 2

.= R2Homeomorphism . (<:X3,Y3:> . [y,z]) by A52, A190, A177, FUNCT_3:49

.= (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] by A52, A180, A190, FUNCT_2:15 ; :: thesis: verum

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

hence
BR-map f is continuous
by JGRAPH_2:10; :: thesis: verum
let p be Point of (Tdisk (o,r)); :: thesis: 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 )

let V be Subset of (Tcircle (o,r)); :: thesis: ( (BR-map f) . p in V & V is open implies ex W being Subset of (Tdisk (o,r)) st

( p in W & W is open & (BR-map f) .: W c= V ) )

assume that

A214: (BR-map f) . p in V and

A215: V is open ; :: thesis: ex W being Subset of (Tdisk (o,r)) st

( p in W & W is open & (BR-map f) .: W c= V )

consider V1 being Subset of (TOP-REAL 2) such that

A216: V1 is open and

A217: V1 /\ ([#] (Tcircle (o,r))) = V by A215, TOPS_2:24;

reconsider p1 = p, fp = f . p as Point of (TOP-REAL 2) by PRE_TOPC:25;

A218: rng R2Homeomorphism = [#] (TOP-REAL 2) by TOPREALA:34, TOPS_2:def 5;

R2Homeomorphism " is being_homeomorphism by TOPREALA:34, TOPS_2:56;

then A219: (R2Homeomorphism ") .: V1 is open by A216, TOPGRP_1:25;

not p is_a_fixpoint_of f by A16;

then p <> f . p ;

then [p1,fp] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) ;

then A220: [p,(f . p)] in OK by XBOOLE_0:def 4;

(BR-map f) . p = (R2Homeomorphism * F) . [p,(f . p)] by A175;

then (R2Homeomorphism * F) . [p1,fp] in V1 by A214, A217, XBOOLE_0:def 4;

then A221: (R2Homeomorphism ") . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism ") .: V1 by FUNCT_2:35;

A222: R2Homeomorphism is one-to-one by TOPREALA:34, TOPS_2:def 5;

A223: dom R2Homeomorphism = the carrier of [:R^1,R^1:] by FUNCT_2:def 1;

then A224: rng F c= dom R2Homeomorphism ;

then ( dom F = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom (R2Homeomorphism * F) = dom F ) by FUNCT_2:def 1, RELAT_1:27;

then A225: ((R2Homeomorphism ") * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism ") .: V1 by A52, A220, A221, FUNCT_1:13;

A226: for x being object st x in dom F holds

((id (dom R2Homeomorphism)) * F) . x = F . x

then dom ((id (dom R2Homeomorphism)) * F) = dom F by A224, RELAT_1:27;

then A229: (id (dom R2Homeomorphism)) * F = F by A226, FUNCT_1:2;

(R2Homeomorphism ") * (R2Homeomorphism * F) = ((R2Homeomorphism ") * R2Homeomorphism) * F by RELAT_1:36

.= (id (dom R2Homeomorphism)) * F by A218, A222, TOPS_2:52 ;

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 A52, A220, A219, A229, A225, JGRAPH_2:10;

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:24;

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:5;

[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;

set ZZ = Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK));

Z c= WW by A235, A238, ZFMISC_1:74;

then Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by XBOOLE_1:27;

then A239: F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) c= F .: W by A234, RELAT_1:123;

consider X1, Y1 being Subset of (TOP-REAL 2) such that

A240: Z = [:X1,Y1:] and

A241: ( X1 is open & Y1 is open ) by A236, A238;

reconsider XX = X1 /\ ([#] (Tdisk (o,r))), YY = Y1 /\ ([#] (Tdisk (o,r))) as open Subset of (Tdisk (o,r)) by A241, TOPS_2:24;

fp in Y1 by A237, A240, ZFMISC_1:87;

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:10;

take W1 = XX /\ M; :: thesis: ( p in W1 & W1 is open & (BR-map f) .: W1 c= V )

p in X1 by A237, A240, ZFMISC_1:87;

then p in XX by XBOOLE_0:def 4;

hence p in W1 by A242, XBOOLE_0:def 4; :: thesis: ( W1 is open & (BR-map f) .: W1 c= V )

thus W1 is open by A243; :: thesis: (BR-map f) .: W1 c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in (BR-map f) .: W1 or b in V )

assume b in (BR-map f) .: W1 ; :: thesis: b in V

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:65;

reconsider a1 = a, fa = f . a as Point of (TOP-REAL 2) by PRE_TOPC:25;

a in M by A245, XBOOLE_0:def 4;

then fa in f .: M by FUNCT_2:35;

then A247: f . a in Y1 by A244, XBOOLE_0:def 4;

not a is_a_fixpoint_of f by A16;

then a <> f . a ;

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 XX by A245, XBOOLE_0:def 4;

then a in X1 by XBOOLE_0:def 4;

then [a,fa] in Z by A240, A247, ZFMISC_1:def 2;

then [a,fa] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by A52, A248, XBOOLE_0:def 4;

then F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) by FUNCT_2:35;

then F . [a1,fa] in F .: W by A239;

then R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A232, FUNCT_2:35;

then A249: (R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A52, A248, FUNCT_2:15;

R2Homeomorphism is onto by A218, FUNCT_2:def 3;

then ( R2Homeomorphism " = R2Homeomorphism " & dom (R2Homeomorphism ") = [#] (TOP-REAL 2) ) by A218, A222, TOPS_2:49, TOPS_2:def 4;

then (R2Homeomorphism * F) . [a1,fa] in V1 by A222, A249, PARTFUN3:1;

then (BR-map f) . a in V1 by A175;

hence b in V by A217, A246, XBOOLE_0:def 4; :: thesis: verum

end;ex W being Subset of (Tdisk (o,r)) st

( p in W & W is open & (BR-map f) .: W c= V )

let V be Subset of (Tcircle (o,r)); :: thesis: ( (BR-map f) . p in V & V is open implies ex W being Subset of (Tdisk (o,r)) st

( p in W & W is open & (BR-map f) .: W c= V ) )

assume that

A214: (BR-map f) . p in V and

A215: V is open ; :: thesis: ex W being Subset of (Tdisk (o,r)) st

( p in W & W is open & (BR-map f) .: W c= V )

consider V1 being Subset of (TOP-REAL 2) such that

A216: V1 is open and

A217: V1 /\ ([#] (Tcircle (o,r))) = V by A215, TOPS_2:24;

reconsider p1 = p, fp = f . p as Point of (TOP-REAL 2) by PRE_TOPC:25;

A218: rng R2Homeomorphism = [#] (TOP-REAL 2) by TOPREALA:34, TOPS_2:def 5;

R2Homeomorphism " is being_homeomorphism by TOPREALA:34, TOPS_2:56;

then A219: (R2Homeomorphism ") .: V1 is open by A216, TOPGRP_1:25;

not p is_a_fixpoint_of f by A16;

then p <> f . p ;

then [p1,fp] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) ;

then A220: [p,(f . p)] in OK by XBOOLE_0:def 4;

(BR-map f) . p = (R2Homeomorphism * F) . [p,(f . p)] by A175;

then (R2Homeomorphism * F) . [p1,fp] in V1 by A214, A217, XBOOLE_0:def 4;

then A221: (R2Homeomorphism ") . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism ") .: V1 by FUNCT_2:35;

A222: R2Homeomorphism is one-to-one by TOPREALA:34, TOPS_2:def 5;

A223: dom R2Homeomorphism = the carrier of [:R^1,R^1:] by FUNCT_2:def 1;

then A224: rng F c= dom R2Homeomorphism ;

then ( dom F = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom (R2Homeomorphism * F) = dom F ) by FUNCT_2:def 1, RELAT_1:27;

then A225: ((R2Homeomorphism ") * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism ") .: V1 by A52, A220, A221, FUNCT_1:13;

A226: for x being object st x in dom F holds

((id (dom R2Homeomorphism)) * F) . x = F . x

proof

dom (id (dom R2Homeomorphism)) = dom R2Homeomorphism
;
let x be object ; :: thesis: ( x in dom F implies ((id (dom R2Homeomorphism)) * F) . x = F . x )

assume A227: x in dom F ; :: thesis: ((id (dom R2Homeomorphism)) * F) . x = F . x

A228: F . x in rng F by A227, FUNCT_1:def 3;

thus ((id (dom R2Homeomorphism)) * F) . x = (id (dom R2Homeomorphism)) . (F . x) by A227, FUNCT_1:13

.= F . x by A223, A228, FUNCT_1:18 ; :: thesis: verum

end;assume A227: x in dom F ; :: thesis: ((id (dom R2Homeomorphism)) * F) . x = F . x

A228: F . x in rng F by A227, FUNCT_1:def 3;

thus ((id (dom R2Homeomorphism)) * F) . x = (id (dom R2Homeomorphism)) . (F . x) by A227, FUNCT_1:13

.= F . x by A223, A228, FUNCT_1:18 ; :: thesis: verum

then dom ((id (dom R2Homeomorphism)) * F) = dom F by A224, RELAT_1:27;

then A229: (id (dom R2Homeomorphism)) * F = F by A226, FUNCT_1:2;

(R2Homeomorphism ") * (R2Homeomorphism * F) = ((R2Homeomorphism ") * R2Homeomorphism) * F by RELAT_1:36

.= (id (dom R2Homeomorphism)) * F by A218, A222, TOPS_2:52 ;

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 A52, A220, A219, A229, A225, JGRAPH_2:10;

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:24;

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:5;

[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;

set ZZ = Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK));

Z c= WW by A235, A238, ZFMISC_1:74;

then Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by XBOOLE_1:27;

then A239: F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) c= F .: W by A234, RELAT_1:123;

consider X1, Y1 being Subset of (TOP-REAL 2) such that

A240: Z = [:X1,Y1:] and

A241: ( X1 is open & Y1 is open ) by A236, A238;

reconsider XX = X1 /\ ([#] (Tdisk (o,r))), YY = Y1 /\ ([#] (Tdisk (o,r))) as open Subset of (Tdisk (o,r)) by A241, TOPS_2:24;

fp in Y1 by A237, A240, ZFMISC_1:87;

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:10;

take W1 = XX /\ M; :: thesis: ( p in W1 & W1 is open & (BR-map f) .: W1 c= V )

p in X1 by A237, A240, ZFMISC_1:87;

then p in XX by XBOOLE_0:def 4;

hence p in W1 by A242, XBOOLE_0:def 4; :: thesis: ( W1 is open & (BR-map f) .: W1 c= V )

thus W1 is open by A243; :: thesis: (BR-map f) .: W1 c= V

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in (BR-map f) .: W1 or b in V )

assume b in (BR-map f) .: W1 ; :: thesis: b in V

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:65;

reconsider a1 = a, fa = f . a as Point of (TOP-REAL 2) by PRE_TOPC:25;

a in M by A245, XBOOLE_0:def 4;

then fa in f .: M by FUNCT_2:35;

then A247: f . a in Y1 by A244, XBOOLE_0:def 4;

not a is_a_fixpoint_of f by A16;

then a <> f . a ;

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 XX by A245, XBOOLE_0:def 4;

then a in X1 by XBOOLE_0:def 4;

then [a,fa] in Z by A240, A247, ZFMISC_1:def 2;

then [a,fa] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by A52, A248, XBOOLE_0:def 4;

then F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) by FUNCT_2:35;

then F . [a1,fa] in F .: W by A239;

then R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A232, FUNCT_2:35;

then A249: (R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A52, A248, FUNCT_2:15;

R2Homeomorphism is onto by A218, FUNCT_2:def 3;

then ( R2Homeomorphism " = R2Homeomorphism " & dom (R2Homeomorphism ") = [#] (TOP-REAL 2) ) by A218, A222, TOPS_2:49, TOPS_2:def 4;

then (R2Homeomorphism * F) . [a1,fa] in V1 by A222, A249, PARTFUN3:1;

then (BR-map f) . a in V1 by A175;

hence b in V by A217, A246, XBOOLE_0:def 4; :: thesis: verum