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; 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); 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]
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]
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]
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;
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)); ( f is without_fixpoints implies BR-map f is continuous )
assume A16:
f is without_fixpoints
; 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]
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]
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]
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):];
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;
( 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
;
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)
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:]
;
( 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;
( [:([#] (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;
Yo .: [:([#] (TOP-REAL 2)),W2:] c= V
let b be
object ;
TARSKI:def 3 ( not b in Yo .: [:([#] (TOP-REAL 2)),W2:] or b in V )
assume
b in Yo .: [:([#] (TOP-REAL 2)),W2:]
;
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;
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):];
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;
( 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
;
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)
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:]
;
( 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;
( [:([#] (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;
Xo .: [:([#] (TOP-REAL 2)),W2:] c= V
let b be
object ;
TARSKI:def 3 ( not b in Xo .: [:([#] (TOP-REAL 2)),W2:] or b in V )
assume
b in Xo .: [:([#] (TOP-REAL 2)),W2:]
;
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;
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):];
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;
( 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
;
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)
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)
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:]
;
( 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;
( [: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;
Dy .: [:W1,W2:] c= V
let b be
object ;
TARSKI:def 3 ( not b in Dy .: [:W1,W2:] or b in V )
assume
b in Dy .: [:W1,W2:]
;
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;
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):];
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;
( 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
;
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)
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)
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:]
;
( 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;
( [: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;
Dx .: [:W1,W2:] c= V
let b be
object ;
TARSKI:def 3 ( not b in Dx .: [:W1,W2:] or b in V )
assume
b in Dx .: [:W1,W2:]
;
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;
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):];
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;
( 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
;
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)
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:]
;
( 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;
( [:([#] (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;
fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V
let b be
object ;
TARSKI:def 3 ( not b in fY2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )
assume
b in fY2 .: [:([#] (TOP-REAL 2)),W1:]
;
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;
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):];
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;
( 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
;
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)
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:]
;
( 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;
( [:([#] (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;
fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V
let b be
object ;
TARSKI:def 3 ( not b in fX2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )
assume
b in fX2 .: [:([#] (TOP-REAL 2)),W1:]
;
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;
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
A142:
now for b being Real st b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) holds
0 >= blet b be
Real;
( 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))
;
0 >= bthen 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;
verum end;
now for b being Real st b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) holds
0 < blet b be
Real;
( 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)))
;
0 < bthen 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);
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;
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));
(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
;
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));
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));
( (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
;
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
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;
( 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;
( W1 is open & (BR-map f) .: W1 c= V )
thus
W1 is
open
by A243;
(BR-map f) .: W1 c= V
let b be
object ;
TARSKI:def 3 ( not b in (BR-map f) .: W1 or b in V )
assume
b in (BR-map f) .: W1
;
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;
verum
end;
hence
BR-map f is continuous
by JGRAPH_2:10; verum