let p be Point of (TOP-REAL 2); :: thesis:
let C be Simple_closed_curve; :: thesis:
let P, B 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 number ; :: 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:29;
A14: the carrier of ((TOP-REAL 2) | A) = A by PRE_TOPC:29;
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:29;
then A18: p in [#] (Tdisk (p,r)) by A15, TOPREAL9:8;
A19: P c= Cl P by PRE_TOPC:48;
ex j being set 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;

assume A20: p in P ; :: thesis:
U misses V by A1, A10, A11, CONNSP_1:37;
hence contradiction by A4, A9, A20, XBOOLE_0:3; :: thesis:

end;

then p in P ` by SUBSET_1:50;
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;
A21: the carrier of ((Tdisk (p,r)) | F1) = F1 by PRE_TOPC:29;
A22: the carrier of ((Tdisk (p,r)) | F3) = F3 by PRE_TOPC:29;
A23: the carrier of ((TOP-REAL 2) | B1) = B1 by PRE_TOPC:29;
A24: A c= B

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

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A27: a in F1 ; :: thesis:
then A28: a in Cl P by XBOOLE_0:def 4;

assume A29: p in Cl P ; :: thesis:
Cl P misses V by A1, A9, A10, A11, Th68;
hence contradiction by A4, A29, XBOOLE_0:3; :: thesis:

end;

hence a in B by A12, A15, A27, A28, ZFMISC_1:64; :: thesis:

end;

then reconsider f1 = id F1 as Function of ((Tdisk (p,r)) | F1),T2B1 by A21, A23, FUNCT_2:9;
f | F3 is Function of F3,A by A14, FUNCT_2:38;
then reconsider g1 = f | F3 as Function of ((Tdisk (p,r)) | F3),T2B1 by A22, A23, A24, FUNCT_2:9;
A30: F1 = [#] ((Tdisk (p,r)) | F1) by PRE_TOPC:29;
A31: F3 = [#] ((Tdisk (p,r)) | F3) by PRE_TOPC:29;
A32: ([#] ((Tdisk (p,r)) | F1)) \/ ([#] ((Tdisk (p,r)) | F3)) = [#] (Tdisk (p,r))

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

suppose p in P ; :: thesis:

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

end;

suppose not p in P ; :: thesis:

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

end;

end;

end;

reconsider DT = [#] (Tdisk (p,r)) as closed Subset of (TOP-REAL 2) by BORSUK_1:def 14, TSEP_1:1;
DT /\ (Cl P) is closed ;
then A34: F1 is closed by TSEP_1:8;
P is_a_component_of C `

take U ; :: according to CONNSP_1:def 6 :: thesis:
thus ( U = P & U is a_component ) by A9, A10; :: thesis:

end;

then P is open by SPRECT_3:18;
then DT /\ (P `) is closed ;
then A35: F3 is closed by TSEP_1:8;
A36: id ((Tdisk (p,r)) | F1) = id F1 by PRE_TOPC:29;
(Tdisk (p,r)) | F1 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then (Tdisk (p,r)) | F1 is SubSpace of T2B1 by A21, A23, A26, TSEP_1:4;
then A37: f1 is continuous by A36, PRE_TOPC:56;
A38: (TOP-REAL 2) | A is SubSpace of T2B1 by A14, A23, A24, TSEP_1:4;
reconsider g2 = g1 as Function of ((Tdisk (p,r)) | F3),((TOP-REAL 2) | A) by A22, FUNCT_2:38;
g2 is continuous by A7, TOPMETR:10;
then A39: g1 is continuous by A38, PRE_TOPC:56;
A40: for x being set st x in Cl P & x in P ` holds
f . x = x

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

end;

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

let x be set ; :: thesis:
assume A44: x in ([#] ((Tdisk (p,r)) | F1)) /\ ([#] ((Tdisk (p,r)) | F3)) ; :: thesis:
then A45: x in [#] ((Tdisk (p,r)) | F1) by XBOOLE_0:def 4;
then A46: x in Cl P by A30, XBOOLE_0:def 4;
x in P ` by A31, A44, XBOOLE_0:def 4;
then A47: f . x = x by A40, A46;
thus f1 . x = x by A30, A45, FUNCT_1:35
.= g1 . x by A31, A44, A47, FUNCT_1:72 ; :: thesis:

end;

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

hereby :: thesis:

assume A51: x in Cl P ; :: thesis:
then A52: x in F1 by XBOOLE_0:def 4;

suppose not x in dom g1 ; :: thesis:

hence g . x = f1 . x by A48, FUNCT_4:12
.= x by A52, FUNCT_1:35 ;
:: thesis:

end;

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

then A54: x in P ` by A22, XBOOLE_0:def 4;
thus g . x = g1 . x by A48, A53, FUNCT_4:14
.= f . x by A22, A53, FUNCT_1:72
.= x by A40, A51, A54 ; :: thesis:

end;

end;

end;

assume x in P ` ; :: thesis:
then A55: x in F3 by XBOOLE_0:def 4;
hence g . x = g1 . x by A22, A48, A50, FUNCT_4:14
.= f . x by A55, FUNCT_1:72 ;
:: thesis: