let p1, p2, p be Point of (TOP-REAL 2); :: thesis:
let C be Simple_closed_curve; :: thesis:
let A, P, B be Subset of (TOP-REAL 2); :: thesis:
let U be Subset of ((TOP-REAL 2) | (C ` )); :: thesis:
let r be positive real number ; :: thesis:
set D = Tdisk p,r;
assume that
A1: A is_an_arc_of p1,p2 and
A2: A c= C and
A3: C c= Ball p,r and
A4: p in U and
A5: (Cl P) /\ (P ` ) c= A and
A6: P c= Ball p,r ; :: 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: B = (cl_Ball p,r) \ {p} ; :: thesis:
reconsider B1 = B as non empty Subset of (TOP-REAL 2) by A11;
reconsider T2B1 = (TOP-REAL 2) | B1 as non empty SubSpace of TOP-REAL 2 ;
A12: the carrier of ((TOP-REAL 2) | (C ` )) = C ` by PRE_TOPC:29;
A13: the carrier of ((TOP-REAL 2) | A) = A by PRE_TOPC:29;
A14: the carrier of (Tdisk p,r) = cl_Ball p,r by BROUWER:3;
A15: Ball p,r c= cl_Ball p,r by TOPREAL9:16;
A16: A <> {} by A1, TOPREAL1:4;
reconsider A1 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:4;
A17: not p in C by A4, A12, XBOOLE_0:def 5;
|.(p - p).| = 0 by TOPRNS_1:29;
then A18: p in [#] (Tdisk p,r) by A14, TOPREAL9:8;
A19: P c= Cl P by PRE_TOPC:48;
then reconsider F1 = (Cl P) /\ ([#] (Tdisk p,r)) as non empty Subset of (Tdisk p,r) by A4, A9, A18, XBOOLE_0:def 4;
A20: Sphere p,r c= cl_Ball p,r by TOPREAL9:17;
A21: Ball p,r misses Sphere p,r by TOPREAL9:19;
consider e being Point of (TOP-REAL 2) such that
A22: e in Sphere p,r by SUBSET_1:10;
not e in P by A6, A21, A22, XBOOLE_0:3;
then e in P ` by SUBSET_1:50;
then reconsider F3 = (P ` ) /\ ([#] (Tdisk p,r)) as non empty Subset of (Tdisk p,r) by A14, A20, A22, XBOOLE_0:def 4;
reconsider T1 = (Tdisk p,r) | F1 as non empty SubSpace of Tdisk p,r ;
reconsider T3 = (Tdisk p,r) | F3 as non empty SubSpace of Tdisk p,r ;
A23: the carrier of T1 = F1 by PRE_TOPC:29;
A24: the carrier of T3 = F3 by PRE_TOPC:29;
A25: the carrier of T2B1 = B1 by PRE_TOPC:29;
A26: A c= B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in A ; :: thesis:
then A27: a in C by A2;
then a in Ball p,r by A3;
hence a in B by A11, A15, A17, A27, ZFMISC_1:64; :: thesis:

end;

A28: F3 c= B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A29: a in F3 ; :: thesis:
then a in P ` by XBOOLE_0:def 4;
then not a in P by XBOOLE_0:def 5;
hence a in B by A4, A9, A11, A14, A29, ZFMISC_1:64; :: thesis:

end;

f | F1 is Function of F1,A by A13, A16, FUNCT_2:38;
then reconsider f1 = f | F1 as Function of T1,T2B1 by A16, A23, A25, A26, FUNCT_2:9;
reconsider g1 = id F3 as Function of T3,T2B1 by A24, A25, A28, FUNCT_2:9;
A30: ( F1 = [#] T1 & F3 = [#] T3 ) by PRE_TOPC:29;
A31: ([#] T1) \/ ([#] T3) = [#] (Tdisk p,r)

proof

thus ([#] T1) \/ ([#] T3) 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 ([#] T1) \/ ([#] T3) by A30, XBOOLE_0:def 3; :: thesis:

end;

suppose not p in P ; :: thesis:

then p in P ` by A14, A32, SUBSET_1:50;
then p in F3 by A32, XBOOLE_0:def 4;
hence p in ([#] T1) \/ ([#] T3) 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;
reconsider f2 = f | F1 as Function of T1,((TOP-REAL 2) | A1) by A23, FUNCT_2:38;
A35: (TOP-REAL 2) | A1 is SubSpace of T2B1 by A13, A25, A26, TSEP_1:4;
T3 is SubSpace of TOP-REAL 2 by TSEP_1:7;
then A36: T3 is SubSpace of T2B1 by A24, A25, A28, TSEP_1:4;
f2 is continuous by A7, TOPMETR:10;
then A37: f1 is continuous by A35, PRE_TOPC:56;
reconsider g2 = id F3 as Function of T3,T3 by A24;
g2 = id T3 by PRE_TOPC:29;
then A38: g1 is continuous by A36, 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 ([#] T1) /\ ([#] T3) holds
f1 . x = g1 . x

proof

let x be set ; :: thesis:
assume A41: x in ([#] T1) /\ ([#] T3) ; :: thesis:
then A42: ( x in [#] T1 & x in [#] T3 ) 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 = f . x by A30, A42, FUNCT_1:72
.= g1 . x by A30, A41, A43, FUNCT_1:35 ; :: 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, A37, 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 T3 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
.= f . x by A48, FUNCT_1:72 ;
:: thesis:

end;

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

then A50: ( x in Cl P & x in P ` ) by A24, A47, XBOOLE_0:def 4;
thus g . x = g1 . x by A44, A49, FUNCT_4:14
.= x by A24, A49, FUNCT_1:35
.= f . 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 A24, A44, A46, FUNCT_4:14
.= x by A51, FUNCT_1:35 ;
:: thesis: