let p1, p2, p be Point of (TOP-REAL 2); :: thesis: for A being Subset of (TOP-REAL 2)
for r being non negative real number st A is_an_arc_of p1,p2 & A is Subset of (Tdisk (p,r)) holds
ex f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A )
let A be Subset of (TOP-REAL 2); :: thesis: for r being non negative real number st A is_an_arc_of p1,p2 & A is Subset of (Tdisk (p,r)) holds
ex f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A )
let r be non negative real number ; :: thesis: ( A is_an_arc_of p1,p2 & A is Subset of (Tdisk (p,r)) implies ex f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A ) )
set D = Tdisk (p,r);
assume that
A1: A is_an_arc_of p1,p2 and
A2: A is Subset of (Tdisk (p,r)) ; :: thesis: ex f being Function of (Tdisk (p,r)),((TOP-REAL 2) | A) st
( f is continuous & f | A = id A )
reconsider A1 = A as non empty Subset of (Tdisk (p,r)) by A1, A2, TOPREAL1:4;
reconsider A2 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:4;
set TA = (TOP-REAL 2) | A2;
consider h being Function of I[01],((TOP-REAL 2) | A2) such that
A3: h is being_homeomorphism and
h . 0 = p1 and
h . 1 = p2 by A1, TOPREAL1:def 2;
A4: L[01] (((#) ((- 1),1)),(((- 1),1) (#))) is being_homeomorphism by TREAL_1:20;
reconsider hh = h as Function of (Closed-Interval-TSpace (0,1)),((TOP-REAL 2) | A2) by TOPMETR:27;
A5: (TOP-REAL 2) | A2 = (Tdisk (p,r)) | A1 by TOPALG_5:4;
then reconsider f = (L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) * (hh ") as Function of ((Tdisk (p,r)) | A1),(Closed-Interval-TSpace ((- 1),1)) ;
A is closed by A1, JORDAN6:12;
then A6: A1 is closed by TSEP_1:12;
hh " is continuous by A3, TOPMETR:27, TOPS_2:def 5;
then consider g being continuous Function of (Tdisk (p,r)),(Closed-Interval-TSpace ((- 1),1)) such that
A7: g | A1 = f by A4, A5, A6, TIETZE:25;
reconsider R = (hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) * g as Function of (Tdisk (p,r)),((TOP-REAL 2) | A) ;
take R ; :: thesis: ( R is continuous & R | A = id A )
(L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) " is continuous by A4, TOPS_2:def 5;
hence R is continuous by A3, TOPMETR:27; :: thesis: R | A = id A
A8: the carrier of ((TOP-REAL 2) | A2) = A1 by PRE_TOPC:29;
A9: dom R = the carrier of (Tdisk (p,r)) by FUNCT_2:def 1;
then A10: dom (R | A) = A by A2, RELAT_1:91;
A11: dom (id A) = A by RELAT_1:71;

now

let a be set ; :: thesis: ( a in dom (R | A) implies (R | A) . a = (id A) . a )
assume A12: a in dom (R | A) ; :: thesis: (R | A) . a = (id A) . a
A13: dom g = the carrier of (Tdisk (p,r)) by FUNCT_2:def 1;
A14: dom ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) * (hh ")) = the carrier of ((TOP-REAL 2) | A2) by FUNCT_2:def 1;
A15: (hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) * (hh ")) = ((hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) * (L[01] (((#) ((- 1),1)),(((- 1),1) (#))))) * (hh ") by RELAT_1:55
.= (hh * (((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ") * (L[01] (((#) ((- 1),1)),(((- 1),1) (#)))))) * (hh ") by RELAT_1:55
.= (hh * (id (Closed-Interval-TSpace (0,1)))) * (hh ") by A4, GRCAT_1:56
.= hh * (hh ") by FUNCT_2:23
.= id ((TOP-REAL 2) | A2) by A3, GRCAT_1:56 ;
thus (R | A) . a = R . a by A10, A12, FUNCT_1:72
.= (hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) . (g . a) by A12, A13, FUNCT_1:23
.= (hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) . (((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) * (hh ")) . a) by A7, A10, A12, FUNCT_1:72
.= (id A) . a by A8, A10, A12, A14, A15, FUNCT_1:23 ; :: thesis: verum

end;

hence R | A = id A by A2, A9, A11, FUNCT_1:9, RELAT_1:91; :: thesis: verum