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_of (TOP-REAL 2) | (C ` ) and
A11: V is_a_component_of (TOP-REAL 2) | (C ` ) 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;

now

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

proof

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;

A26: F1 c= B

proof

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;

now

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) & F3 = [#] ((Tdisk p,r) | F3) ) by PRE_TOPC:29;
A31: ([#] ((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 A30, XBOOLE_1:8; :: according to XBOOLE_0:def 10 :: thesis:
let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A32: p in [#] (Tdisk p,r) ; :: thesis:

per cases ;

suppose p in P ; :: thesis:

then p in F1 by A19, A32, 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, A32, SUBSET_1:50;
then p in F3 by A32, XBOOLE_0:def 4;
hence p in ([#] ((Tdisk p,r) | F1)) \/ ([#] ((Tdisk p,r) | F3)) by A30, XBOOLE_0:def 3; :: thesis:

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 by TOPS_1:35;
then A33: F1 is closed by TSEP_1:8;
P is_a_component_of C `

proof

take U ; :: according to CONNSP_1:def 6 :: thesis:
thus ( U = P & U is_a_component_of (TOP-REAL 2) | (C ` ) ) by A9, A10; :: thesis:

end;

then P is open by SPRECT_3:18;
then P ` is closed ;
then DT /\ (P ` ) is closed by TOPS_1:35;
then A34: F3 is closed by TSEP_1:8;
A35: 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 A36: f1 is continuous by A35, PRE_TOPC:56;
A37: (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 A38: g1 is continuous by A37, PRE_TOPC:56;
A39: for x being set st x in Cl P & x in P ` holds
f . x = x

proof

let x be set ; :: thesis:
assume ( x in Cl P & x in P ` ) ; :: thesis:
then A40: x in (Cl P) /\ (P ` ) by XBOOLE_0:def 4;
then (id A) . x = x by A5, FUNCT_1:35;
hence f . x = x by A5, A8, A40, 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

proof

let x be set ; :: thesis:
assume A41: x in ([#] ((Tdisk p,r) | F1)) /\ ([#] ((Tdisk p,r) | F3)) ; :: thesis:
then A42: ( x in [#] ((Tdisk p,r) | F1) & x in [#] ((Tdisk p,r) | F3) ) by XBOOLE_0:def 4;
then ( x in Cl P & x in P ` ) by A30, XBOOLE_0:def 4;
then A43: f . x = x by A39;
thus f1 . x = x by A30, A42, FUNCT_1:35
.= g1 . x by A30, A41, A43, FUNCT_1:72 ; :: thesis:

end;

then consider g being Function of (Tdisk p,r),((TOP-REAL 2) | B) such that
A44: g = f1 +* g1 and
A45: g is continuous by A30, A31, A33, A34, A36, A38, JGRAPH_2:9;
take g ; :: thesis:
thus g is continuous by A45; :: thesis:
let x be Point of (Tdisk p,r); :: thesis:
A46: dom g1 = the carrier of ((Tdisk p,r) | F3) by FUNCT_2:def 1;

hereby :: thesis:

assume A47: x in Cl P ; :: thesis:
then A48: x in F1 by XBOOLE_0:def 4;

per cases ;

suppose not x in dom g1 ; :: thesis:

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

end;

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

then A50: ( x in Cl P & x in P ` ) by A22, A47, XBOOLE_0:def 4;
thus g . x = g1 . x by A44, A49, FUNCT_4:14
.= f . x by A22, A49, FUNCT_1:72
.= x by A39, A50 ; :: thesis:

end;

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