let p, p1, p2 be Point of (TOP-REAL 2); :: thesis:
let C be Simple_closed_curve; :: thesis:
let A, B, P be Subset of (TOP-REAL 2); :: thesis:
let U be Subset of ((TOP-REAL 2) | (C `)); :: thesis:
let r be positive Real; :: 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 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:8;
A13: the carrier of ((TOP-REAL 2) | A) = A by PRE_TOPC:8;
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:1;
reconsider A1 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
A17: not p in C by A4, A12, XBOOLE_0:def 5;
|.(p - p).| = 0 by TOPRNS_1:28;
then A18: p in [#] (Tdisk (p,r)) by A14, TOPREAL9:8;
A19: P c= Cl P by PRE_TOPC:18;
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:4;
not e in P by A6, A21, A22, XBOOLE_0:3;
then e in P ` by SUBSET_1:29;
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:8;
A24: the carrier of T3 = F3 by PRE_TOPC:8;
A25: the carrier of T2B1 = B1 by PRE_TOPC:8;
A26: A c= B

proof

let a be object ; :: 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:56; :: thesis:

end;

A28: F3 c= B

proof

let a be object ; :: 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:56; :: thesis:

end;

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

proof

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

per cases ;

suppose p in P ; :: thesis:

then p in F1 by A19, A33, 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, A33, SUBSET_1:29;
then p in F3 by A33, XBOOLE_0:def 4;
hence p in ([#] T1) \/ ([#] T3) by A31, 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 A34: 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 A35: F3 is closed by TSEP_1:8;
reconsider f2 = f | F1 as Function of T1,((TOP-REAL 2) | A1) by A23, FUNCT_2:32;
A36: (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 A37: T3 is SubSpace of T2B1 by A24, A25, A28, TSEP_1:4;
f2 is continuous by A7, TOPMETR:7;
then A38: f1 is continuous by A36, PRE_TOPC:26;
reconsider g2 = id F3 as Function of T3,T3 by A24;
g2 = id T3 by PRE_TOPC:8;
then A39: g1 is continuous by A37, PRE_TOPC:26;
A40: for x being set st x in Cl P & x in P ` holds
f . x = x

proof

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:18;
hence f . x = x by A5, A8, A43, FUNCT_1:49; :: thesis:

end;

for x being object st x in ([#] T1) /\ ([#] T3) holds
f1 . x = g1 . x

proof

let x be object ; :: thesis:
assume A44: x in ([#] T1) /\ ([#] T3) ; :: thesis:
then A45: x in [#] T1 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 = f . x by A30, A45, FUNCT_1:49
.= g1 . x by A31, A44, A47, FUNCT_1:18 ; :: 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, A38, A39, JGRAPH_2:1;
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 T3 by FUNCT_2:def 1;

hereby :: thesis:

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

per cases ;

suppose not x in dom g1 ; :: thesis:

hence g . x = f1 . x by A48, FUNCT_4:11
.= f . x by A52, FUNCT_1:49 ;
:: thesis:

end;

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

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

end;

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