let o, p be Point of (TOP-REAL 2); :: thesis:
let r be positive real number ; :: thesis:
assume A1: p is Point of (Tdisk o,r) ; :: thesis:
set D = Tdisk o,r;
set cB = cl_Ball o,r;
set Bp = (cl_Ball o,r) \ {p};
set OK = [:((cl_Ball o,r) \ {p}),{p}:];
set D1 = (TOP-REAL 2) | ((cl_Ball o,r) \ {p});
set D2 = (TOP-REAL 2) | {p};
set S1 = Tcircle o,r;
A2: p in {p} by TARSKI:def 1;
A3: the carrier of (Tdisk o,r) = cl_Ball o,r by BROUWER:3;
A4: the carrier of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})) = (cl_Ball o,r) \ {p} by PRE_TOPC:29;
A5: the carrier of ((TOP-REAL 2) | {p}) = {p} by PRE_TOPC:29;
set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:];
set gg = DiskProj o,r,p;
set xo = diffX2_1 o;
set yo = diffX2_2 o;
set dx = diffX1_X2_1 ;
set dy = diffX1_X2_2 ;
set fx2 = Proj2_1 ;
set fy2 = Proj2_2 ;
reconsider rr = r ^2 as Real by XREAL_0:def 1;
set f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr;
reconsider f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by Lm6;
set Zf1 = f1 | [:((cl_Ball o,r) \ {p}),{p}:];
set Zfx2 = Proj2_1 | [:((cl_Ball o,r) \ {p}),{p}:];
set Zfy2 = Proj2_2 | [:((cl_Ball o,r) \ {p}),{p}:];
set Zdx = diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:];
set Zdy = diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:];
set Zxo = (diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:];
set Zyo = (diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:];
set xx = ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]);
set yy = ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]);
set m = ((diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]));
A6: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) = [:((cl_Ball o,r) \ {p}),{p}:] by PRE_TOPC:29;
A7: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z] by FUNCT_1:72; :: thesis:

end;

A8: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z] by FUNCT_1:72; :: thesis:

end;

A9: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (Proj2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = Proj2_1 . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence (Proj2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = Proj2_1 . [y,z] by FUNCT_1:72; :: thesis:

end;

A10: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (Proj2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = Proj2_2 . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence (Proj2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = Proj2_2 . [y,z] by FUNCT_1:72; :: thesis:

end;

A11: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (f1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = f1 . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence (f1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = f1 . [y,z] by FUNCT_1:72; :: thesis:

end;

A12: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z] by FUNCT_1:72; :: thesis:

end;

A13: for y being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z]

proof

let y be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let z be Point of ((TOP-REAL 2) | {p}); :: thesis:
[y,z] in [:((cl_Ball o,r) \ {p}),{p}:] by A4, A5, ZFMISC_1:def 2;
hence ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z] by FUNCT_1:72; :: thesis:

end;

now

now

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

end;

hence 0 < b by A15, A18, A28; :: thesis:

end;

now

let b be real number ; :: thesis:
assume b in rng (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) - (f1 | [:((cl_Ball o,r) \ {p}),{p}:])) ; :: thesis:
then consider a being set such that
A32: a in dom (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) - (f1 | [:((cl_Ball o,r) \ {p}),{p}:])) and
A33: (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) - (f1 | [:((cl_Ball o,r) \ {p}),{p}:])) . a = b by FUNCT_1:def 5;
consider y, z being set such that
A34: y in (cl_Ball o,r) \ {p} and
A35: z in {p} and
A36: a = [y,z] by A6, A32, ZFMISC_1:def 2;
reconsider y = y, z = z as Point of (TOP-REAL 2) by A34, A35;
set r3 = (z `1 ) - (o `1 );
set r4 = (z `2 ) - (o `2 );
A37: (f1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = f1 . [y,z] by A4, A5, A11, A34, A35;
A38: ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z] by A4, A5, A12, A34, A35;
A39: ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z] by A4, A5, A13, A34, A35;
A40: [y,z] = [([y,z] `1 ),([y,z] `2 )] by Lm5, MCART_1:23;
A41: (diffX2_1 o) . [y,z] = (([y,z] `2 ) `1 ) - (o `1 ) by Def1;
A42: z = [y,z] `2 by A40, ZFMISC_1:33;
A43: (diffX2_2 o) . [y,z] = (([y,z] `2 ) `2 ) - (o `2 ) by Def2;
A44: (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) - (f1 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,z] = (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) . [y,z]) - ((f1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z]) by A32, A36, VALUED_1:13
.= (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) . [y,z]) - (r ^2 ) by A37, FUNCOP_1:13
.= (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,z]) + ((((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,z])) - (r ^2 ) by A32, A36, VALUED_1:1
.= (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z]) * (((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,z])) + ((((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,z])) - (r ^2 ) by VALUED_1:5
.= ((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 ) by A38, A39, A41, A42, A43, VALUED_1:5 ;
z = p by A35, TARSKI:def 1;
then |.(z - o).| <= r by A1, A3, TOPREAL9:8;
then A45: |.(z - o).| ^2 <= r ^2 by SQUARE_1:77;
|.(z - o).| ^2 = (((z - o) `1 ) ^2 ) + (((z - o) `2 ) ^2 ) by JGRAPH_1:46
.= (((z `1 ) - (o `1 )) ^2 ) + (((z - o) `2 ) ^2 ) by TOPREAL3:8
.= (((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 ) by TOPREAL3:8 ;
then ((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 ) <= (r ^2 ) - (r ^2 ) by A45, XREAL_1:11;
hence 0 >= b by A33, A36, A44; :: thesis:

end;

proof

let x be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
consider y being Point of (TOP-REAL 2) such that
A47: x = y and
A48: (DiskProj o,r,p) . x = HC p,y,o,r by A1, Def7;
A49: x <> p by A4, ZFMISC_1:64;
A50: [y,p] in [:((cl_Ball o,r) \ {p}),{p}:] by A2, A4, A47, ZFMISC_1:def 2;
set r1 = (y `1 ) - (p `1 );
set r2 = (y `2 ) - (p `2 );
set r3 = (p `1 ) - (o `1 );
set r4 = (p `2 ) - (o `2 );
set l = ((- ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 ))))) + (sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 ));
A51: [y,p] = [([y,p] `1 ),([y,p] `2 )] by Lm5, MCART_1:23;
then A52: y = [y,p] `1 by ZFMISC_1:33;
A53: p = [y,p] `2 by A51, ZFMISC_1:33;
A54: Proj2_1 . [y,p] = ([y,p] `2 ) `1 by Def5;
A55: Proj2_2 . [y,p] = ([y,p] `2 ) `2 by Def6;
A56: diffX1_X2_1 . [y,p] = (([y,p] `1 ) `1 ) - (([y,p] `2 ) `1 ) by Def3;
A57: diffX1_X2_2 . [y,p] = (([y,p] `1 ) `2 ) - (([y,p] `2 ) `2 ) by Def4;
A58: (diffX2_1 o) . [y,p] = (([y,p] `2 ) `1 ) - (o `1 ) by Def1;
A59: (diffX2_2 o) . [y,p] = (([y,p] `2 ) `2 ) - (o `2 ) by Def2;
A60: dom X3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) by FUNCT_2:def 1;
A61: dom Y3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) by FUNCT_2:def 1;
A62: dom ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) by FUNCT_2:def 1;
A63: p is Point of ((TOP-REAL 2) | {p}) by A5, TARSKI:def 1;
then A64: (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p] = diffX1_X2_1 . [y,p] by A7, A47;
A65: (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p] = diffX1_X2_2 . [y,p] by A8, A47, A63;
A66: (f1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p] = f1 . [y,p] by A11, A47, A63;
A67: ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p] = (diffX2_1 o) . [y,p] by A12, A47, A63;
A68: ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p] = (diffX2_2 o) . [y,p] by A13, A47, A63;
A69: m . [y,p] = (((diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) + (((diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by A6, A50, VALUED_1:1
.= (((diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) * ((diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p])) + (((diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by VALUED_1:5
.= (((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 ) by A52, A53, A56, A57, A64, A65, VALUED_1:5 ;
A70: (((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p] = (((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) * ((diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) by VALUED_1:5;
A71: (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p] = (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) * ((diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) by VALUED_1:5;
A72: ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) . [y,p] = ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) + ((((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by A6, A50, VALUED_1:1;
then A73: (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) . [y,p] = ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 by A52, A53, A56, A57, A58, A59, A64, A65, A67, A68, A70, A71, VALUED_1:5;
A74: p2 . [y,p] = (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) . [y,p]) - ((f1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) by A6, A31, A50, VALUED_1:13
.= (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]))) . [y,p]) - (r ^2 ) by A66, FUNCOP_1:13
.= (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) + ((((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p])) - (r ^2 ) by A6, A50, VALUED_1:1
.= (((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) * (((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p])) + ((((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p])) - (r ^2 ) by VALUED_1:5
.= ((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 ) by A53, A58, A59, A67, A68, VALUED_1:5 ;
dom (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2))) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) by FUNCT_2:def 1;
then A75: (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2))) . [y,p] = sqrt (((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)) . [y,p]) by A6, A50, PARTFUN3:def 5
.= sqrt (((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) . [y,p]) - ((m (#) p2) . [y,p])) by A6, A50, A62, VALUED_1:13
.= sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))) by A69, A73, A74, VALUED_1:5 ;
dom (((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) / m) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) by FUNCT_2:def 1;
then A76: (((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) / m) . [y,p] = (((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) . [y,p]) * ((m . [y,p]) " ) by A6, A50, RFUNCT_1:def 4
.= (((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) . [y,p]) / (m . [y,p]) by XCMPLX_0:def 9
.= (((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) . [y,p]) + ((sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2))) . [y,p])) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) by A6, A50, A69, VALUED_1:1
.= ((- ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 ))))) + (sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) by A52, A53, A56, A57, A58, A59, A64, A65, A67, A68, A70, A71, A72, A75, VALUED_1:8 ;
A77: X3 . [y,p] = ((Proj2_1 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) + (((((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by A6, A50, VALUED_1:1
.= (p `1 ) + (((((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by A9, A47, A53, A54, A63
.= (p `1 ) + ((((- ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 ))))) + (sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 ))) * ((y `1 ) - (p `1 ))) by A52, A53, A56, A64, A76, VALUED_1:5 ;
A78: Y3 . [y,p] = ((Proj2_2 | [:((cl_Ball o,r) \ {p}),{p}:]) . [y,p]) + (((((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by A6, A50, VALUED_1:1
.= (p `2 ) + (((((- ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball o,r) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball o,r) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_2 | [:((cl_Ball o,r) \ {p}),{p}:])) . [y,p]) by A10, A47, A53, A55, A63
.= (p `2 ) + ((((- ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 ))))) + (sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 ))) * ((y `2 ) - (p `2 ))) by A52, A53, A57, A65, A76, VALUED_1:5 ;
A79: y in (cl_Ball o,r) \ {p} by A4, A47;
(cl_Ball o,r) \ {p} c= cl_Ball o,r by XBOOLE_1:36;
hence (DiskProj o,r,p) . x = |[((p `1 ) + ((((- ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 ))))) + (sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 ))) * ((y `1 ) - (p `1 )))),((p `2 ) + ((((- ((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 ))))) + (sqrt ((((((p `1 ) - (o `1 )) * ((y `1 ) - (p `1 ))) + (((p `2 ) - (o `2 )) * ((y `2 ) - (p `2 )))) ^2 ) - (((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 )) * (((((p `1 ) - (o `1 )) ^2 ) + (((p `2 ) - (o `2 )) ^2 )) - (r ^2 )))))) / ((((y `1 ) - (p `1 )) ^2 ) + (((y `2 ) - (p `2 )) ^2 ))) * ((y `2 ) - (p `2 ))))]| by A1, A3, A47, A48, A49, A79, BROUWER:8
.= R2Homeomorphism . [(X3 . [y,p]),(Y3 . [y,p])] by A77, A78, TOPREALA:def 2
.= R2Homeomorphism . (<:X3,Y3:> . [y,p]) by A6, A50, A60, A61, FUNCT_3:69
.= (R2Homeomorphism * <:X3,Y3:>) . [x,p] by A6, A47, A50, FUNCT_2:21 ;
:: thesis:

end;

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

proof

let pp be Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})); :: thesis:
let V be Subset of (Tcircle o,r); :: thesis:
assume that
A81: (DiskProj o,r,p) . pp in V and
A82: V is open ; :: thesis:
reconsider p1 = pp, fp = p as Point of (TOP-REAL 2) by PRE_TOPC:55;
A83: [pp,p] in [:((cl_Ball o,r) \ {p}),{p}:] by A2, A4, ZFMISC_1:def 2;
consider V1 being Subset of (TOP-REAL 2) such that
A84: V1 is open and
A85: V1 /\ ([#] (Tcircle o,r)) = V by A82, TOPS_2:32;
A86: (DiskProj o,r,p) . pp = (R2Homeomorphism * F) . [pp,p] by A46;
R2Homeomorphism " is being_homeomorphism by TOPREALA:56, TOPS_2:70;
then A87: (R2Homeomorphism " ) .: V1 is open by A84, TOPGRP_1:25;
A88: dom F = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) by FUNCT_2:def 1;
A89: dom R2Homeomorphism = the carrier of [:R^1 ,R^1 :] by FUNCT_2:def 1;
then A90: rng F c= dom R2Homeomorphism ;
then A91: dom (R2Homeomorphism * F) = dom F by RELAT_1:46;
A92: rng R2Homeomorphism = [#] (TOP-REAL 2) by TOPREALA:56, TOPS_2:def 5;
A93: (R2Homeomorphism " ) * (R2Homeomorphism * F) = ((R2Homeomorphism " ) * R2Homeomorphism ) * F by RELAT_1:55
.= (id (dom R2Homeomorphism )) * F by A92, TOPREALA:56, TOPS_2:65 ;
dom (id (dom R2Homeomorphism )) = dom R2Homeomorphism by RELAT_1:71;
then A94: dom ((id (dom R2Homeomorphism )) * F) = dom F by A90, RELAT_1:46;
for x being set st x in dom F holds
((id (dom R2Homeomorphism )) * F) . x = F . x

proof

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

end;

then A97: (id (dom R2Homeomorphism )) * F = F by A94, FUNCT_1:9;
(R2Homeomorphism * F) . [p1,fp] in V1 by A81, A85, A86, XBOOLE_0:def 4;
then (R2Homeomorphism " ) . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism " ) .: V1 by FUNCT_2:43;
then ((R2Homeomorphism " ) * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism " ) .: V1 by A6, A83, A88, A91, FUNCT_1:23;
then consider W being Subset of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]) such that
A98: [p1,fp] in W and
A99: W is open and
A100: F .: W c= (R2Homeomorphism " ) .: V1 by A6, A83, A87, A93, A97, JGRAPH_2:20;
consider WW being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A101: WW is open and
A102: WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:])) = W by A99, TOPS_2:32;
consider SF being Subset-Family of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A103: WW = union SF and
A104: 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 A101, BORSUK_1:45;
[p1,fp] in WW by A98, A102, XBOOLE_0:def 4;
then consider Z being set such that
A105: [p1,fp] in Z and
A106: Z in SF by A103, TARSKI:def 4;
consider X1, Y1 being Subset of (TOP-REAL 2) such that
A107: Z = [:X1,Y1:] and
A108: X1 is open and
Y1 is open by A104, A106;
set ZZ = Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]));
reconsider XX = X1 /\ ([#] ((TOP-REAL 2) | ((cl_Ball o,r) \ {p}))) as open Subset of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})) by A108, TOPS_2:32;
take XX ; :: thesis:
pp in X1 by A105, A107, ZFMISC_1:106;
hence pp in XX by XBOOLE_0:def 4; :: thesis:
thus XX is open ; :: thesis:
let b be set ; :: according to TARSKI:def 3 :: thesis:
assume b in (DiskProj o,r,p) .: XX ; :: thesis:
then consider a being Point of ((TOP-REAL 2) | ((cl_Ball o,r) \ {p})) such that
A109: a in XX and
A110: b = (DiskProj o,r,p) . a by FUNCT_2:116;
reconsider a1 = a, fa = fp as Point of (TOP-REAL 2) by PRE_TOPC:55;
A111: a in X1 by A109, XBOOLE_0:def 4;
A112: [a,p] in [:((cl_Ball o,r) \ {p}),{p}:] by A2, A4, ZFMISC_1:def 2;
fa in Y1 by A105, A107, ZFMISC_1:106;
then [a,fa] in Z by A107, A111, ZFMISC_1:def 2;
then [a,fa] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:])) by A6, A112, XBOOLE_0:def 4;
then A113: F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]))) by FUNCT_2:43;
A114: R2Homeomorphism " = R2Homeomorphism " by A92, TOPREALA:56, TOPS_2:def 4;
A115: dom (R2Homeomorphism " ) = [#] (TOP-REAL 2) by A92, TOPREALA:56, TOPS_2:62;
Z c= WW by A103, A106, ZFMISC_1:92;
then Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:])) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:])) by XBOOLE_1:27;
then F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball o,r) \ {p}),{p}:]))) c= F .: W by A102, RELAT_1:156;
then F . [a1,fa] in F .: W by A113;
then R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism " ) .: V1) by A100, FUNCT_2:43;
then (R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism " ) .: V1) by A6, A112, FUNCT_2:21;
then (R2Homeomorphism * F) . [a1,fa] in V1 by A114, A115, PARTFUN3:1, TOPREALA:56;
then (DiskProj o,r,p) . a in V1 by A46;
hence b in V by A85, A110, XBOOLE_0:def 4; :: thesis:

end;

hence DiskProj o,r,p is continuous by JGRAPH_2:20; :: thesis: