set R = R2Homeomorphism ;
defpred S1[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = x2 `1 );
defpred S2[ 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 S3[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x2 `1) - (o `1) );
defpred S4[ 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 S3[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S3[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: S3[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 xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A3: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S3[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 S1[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S1[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: S1[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 fx2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A6: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S1[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 S4[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S4[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: S4[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 yo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A9: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S4[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;
A12: now :: thesis: not o = the Point of (Tcircle (o,r))
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;
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
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 S5[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = x2 `2 );
defpred S6[ 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 S6[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S6[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: S6[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 dy being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A19: for y being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S6[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 S5[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S5[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: S5[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 fy2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A22: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S5[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 S2[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; :: thesis: ex r being Element of REAL st S2[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: S2[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 dx being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A25: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S2[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 )
proof
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)
proof
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;
then reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset 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;
then Yo is continuous by JGRAPH_2:10;
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
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)
proof
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;
then reconsider W2 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset 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;
then Xo is continuous by JGRAPH_2:10;
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
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)
proof
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;
A60: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
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
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;
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) ;
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;
then Dy is continuous by JGRAPH_2:10;
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
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)
proof
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;
A87: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
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
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;
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) ;
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;
then Dx is continuous by JGRAPH_2:10;
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
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)
proof
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;
then reconsider W1 = { |[x,y]| where x, y is Real : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset 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;
then fY2 is continuous by JGRAPH_2:10;
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
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)
proof
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;
then reconsider W1 = { |[x,y]| where x, y is Real : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset 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;
then fX2 is continuous by JGRAPH_2:10;
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;
A142: now :: thesis: for b being Real st b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) holds
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;
now :: thesis: for b being Real st b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) holds
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);
A166: now :: thesis: not (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) = 0
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;
consider x3, x4 being Point of (TOP-REAL 2) such that
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;
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;
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
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;
( X3 is continuous & Y3 is continuous ) by JORDAN5A:27;
then reconsider F = <:X3,Y3:> as continuous Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[:R^1,R^1:] by YELLOW12:41;
for p being Point of (Tdisk (o,r))
for V being Subset of (Tcircle (o,r)) st (BR-map f) . p in V & V is open holds
ex W being Subset of (Tdisk (o,r)) st
( p in W & W is open & (BR-map f) .: W c= V )
proof
let p be Point of (Tdisk (o,r)); :: thesis: 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
proof
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;
dom (id (dom R2Homeomorphism)) = dom R2Homeomorphism ;
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;
hence BR-map f is continuous by JGRAPH_2:10; :: thesis: verum