let p be Point of (TOP-REAL 2); :: thesis:
let C be Simple_closed_curve; :: thesis:
let B, P be Subset of (TOP-REAL 2); :: thesis:
let U, V be Subset of ((TOP-REAL 2) | (C `)); :: thesis:
let A be non empty Subset of (TOP-REAL 2); :: thesis:
assume A1: U <> V ; :: thesis:
let r be positive Real; :: thesis:
set D = Tdisk (p,r);
assume that
A2: A c= C and
A3: C c= Ball (p,r) and
A4: p in V and
A5: (Cl P) /\ (P `) c= A and
A6: Ball (p,r) meets P ; :: thesis:
let f be Function of (Tdisk (p,r)),((TOP-REAL 2) | A); :: thesis:
assume that
A7: f is continuous and
A8: f | A = id A and
A9: U = P and
A10: U is a_component and
A11: V is a_component and
A12: B = (cl_Ball (p,r)) \ {p} ; :: thesis:
reconsider B1 = B as non empty Subset of (TOP-REAL 2) by A12;
reconsider T2B1 = (TOP-REAL 2) | B1 as non empty SubSpace of TOP-REAL 2 ;
A13: the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
A14: the carrier of ((TOP-REAL 2) | A) = A by PRE_TOPC:8;
A15: the carrier of (Tdisk (p,r)) = cl_Ball (p,r) by BROUWER:3;
A16: Ball (p,r) c= cl_Ball (p,r) by TOPREAL9:16;
A17: not p in C by A4, A13, XBOOLE_0:def 5;
|.(p - p).| = 0 by TOPRNS_1:28;
then A18: p in [#] (Tdisk (p,r)) by A15, TOPREAL9:8;
A19: P c= Cl P by PRE_TOPC:18;
ex j being object st
( j in Ball (p,r) & j in P ) by A6, XBOOLE_0:3;
then reconsider F1 = (Cl P) /\ ([#] (Tdisk (p,r))) as non empty Subset of (Tdisk (p,r)) by A15, A16, A19, XBOOLE_0:def 4;
not p in P by A1, A10, A11, CONNSP_1:35, A4, A9, XBOOLE_0:3;
then p in P ` by SUBSET_1:29;
then reconsider F3 = (P `) /\ ([#] (Tdisk (p,r))) as non empty Subset of (Tdisk (p,r)) by A18, XBOOLE_0:def 4;
set T1 = (Tdisk (p,r)) | F1;
set T3 = (Tdisk (p,r)) | F3;
A20: the carrier of ((Tdisk (p,r)) | F1) = F1 by PRE_TOPC:8;
A21: the carrier of ((Tdisk (p,r)) | F3) = F3 by PRE_TOPC:8;
A22: the carrier of ((TOP-REAL 2) | B1) = B1 by PRE_TOPC:8;
A23: A c= B

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in A ; :: thesis:
then A24: a in C by A2;
then a in Ball (p,r) by A3;
hence a in B by A12, A16, A17, A24, ZFMISC_1:56; :: thesis:

end;

A25: F1 c= B

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: a in F1 ; :: thesis:
then A27: a in Cl P by XBOOLE_0:def 4;
not p in Cl P by A4, XBOOLE_0:3, A1, A9, A10, A11, Th68;
hence a in B by A12, A15, A26, A27, ZFMISC_1:56; :: thesis:

end;

then reconsider f1 = id F1 as Function of ((Tdisk (p,r)) | F1),T2B1 by A20, A22, FUNCT_2:7;
f | F3 is Function of F3,A by A14;
then reconsider g1 = f | F3 as Function of ((Tdisk (p,r)) | F3),T2B1 by A21, A22, A23, FUNCT_2:7;
A28: F1 = [#] ((Tdisk (p,r)) | F1) by PRE_TOPC:8;
A29: F3 = [#] ((Tdisk (p,r)) | F3) by PRE_TOPC:8;
A30: ([#] ((Tdisk (p,r)) | F1)) \/ ([#] ((Tdisk (p,r)) | F3)) = [#] (Tdisk (p,r))

proof

thus ([#] ((Tdisk (p,r)) | F1)) \/ ([#] ((Tdisk (p,r)) | F3)) c= [#] (Tdisk (p,r)) by A28, A29, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis:
let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A31: p in [#] (Tdisk (p,r)) ; :: thesis:

per cases ;

suppose p in P ; :: thesis:

then p in F1 by A19, A31, XBOOLE_0:def 4;
hence p in ([#] ((Tdisk (p,r)) | F1)) \/ ([#] ((Tdisk (p,r)) | F3)) by A28, XBOOLE_0:def 3; :: thesis:

end;

suppose not p in P ; :: thesis:

then p in P ` by A15, A31, SUBSET_1:29;
then p in F3 by A31, XBOOLE_0:def 4;
hence p in ([#] ((Tdisk (p,r)) | F1)) \/ ([#] ((Tdisk (p,r)) | F3)) by A29, XBOOLE_0:def 3; :: thesis:

end;

reconsider DT = [#] (Tdisk (p,r)) as closed Subset of (TOP-REAL 2) by BORSUK_1:def 11, TSEP_1:1;
DT /\ (Cl P) is closed ;
then A32: F1 is closed by TSEP_1:8;
P is_a_component_of C ` by A9, A10;
then P is open by SPRECT_3:8;
then DT /\ (P `) is closed ;
then A33: F3 is closed by TSEP_1:8;
A34: id ((Tdisk (p,r)) | F1) = id F1 by PRE_TOPC:8;
(Tdisk (p,r)) | F1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then (Tdisk (p,r)) | F1 is SubSpace of T2B1 by A20, A22, A25, TSEP_1:4;
then A35: f1 is continuous by A34, PRE_TOPC:26;
A36: (TOP-REAL 2) | A is SubSpace of T2B1 by A14, A22, A23, TSEP_1:4;
reconsider g2 = g1 as Function of ((Tdisk (p,r)) | F3),((TOP-REAL 2) | A) by A21;
g2 is continuous by A7, TOPMETR:7;
then A37: g1 is continuous by A36, PRE_TOPC:26;
A38: for x being set st x in Cl P & x in P ` holds
f . x = x

proof

let x be set ; :: thesis:
assume that
A39: x in Cl P and
A40: x in P ` ; :: thesis:
A41: x in (Cl P) /\ (P `) by A39, A40, XBOOLE_0:def 4;
then (id A) . x = x by A5, FUNCT_1:18;
hence f . x = x by A5, A8, A41, FUNCT_1:49; :: thesis:

end;

for x being object st x in ([#] ((Tdisk (p,r)) | F1)) /\ ([#] ((Tdisk (p,r)) | F3)) holds
f1 . x = g1 . x

proof

let x be object ; :: thesis:
assume A42: x in ([#] ((Tdisk (p,r)) | F1)) /\ ([#] ((Tdisk (p,r)) | F3)) ; :: thesis:
then A43: x in [#] ((Tdisk (p,r)) | F1) by XBOOLE_0:def 4;
then A44: x in Cl P by A28, XBOOLE_0:def 4;
x in P ` by A29, A42, XBOOLE_0:def 4;
then A45: f . x = x by A38, A44;
thus f1 . x = x by A28, A43, FUNCT_1:18
.= g1 . x by A29, A42, A45, FUNCT_1:49 ; :: thesis:

end;

then consider g being Function of (Tdisk (p,r)),((TOP-REAL 2) | B) such that
A46: g = f1 +* g1 and
A47: g is continuous by A28, A29, A30, A32, A33, A35, A37, JGRAPH_2:1;
take g ; :: thesis:
thus g is continuous by A47; :: thesis:
let x be Point of (Tdisk (p,r)); :: thesis:
A48: dom g1 = the carrier of ((Tdisk (p,r)) | F3) by FUNCT_2:def 1;

hereby :: thesis:

assume A49: x in Cl P ; :: thesis:
then A50: x in F1 by XBOOLE_0:def 4;

per cases ;

suppose not x in dom g1 ; :: thesis:

hence g . x = f1 . x by A46, FUNCT_4:11
.= x by A50, FUNCT_1:18 ;
:: thesis:

end;

suppose A51: x in dom g1 ; :: thesis:

then A52: x in P ` by A21, XBOOLE_0:def 4;
thus g . x = g1 . x by A46, A51, FUNCT_4:13
.= f . x by A21, A51, FUNCT_1:49
.= x by A38, A49, A52 ; :: thesis:

end;

assume x in P ` ; :: thesis:
then A53: x in F3 by XBOOLE_0:def 4;
hence g . x = g1 . x by A21, A46, A48, FUNCT_4:13
.= f . x by A53, FUNCT_1:49 ;
:: thesis: