let p, p1, p2 be Point of (TOP-REAL 2); :: thesis: for A being Subset of (TOP-REAL 2)
for r being non negative Real 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 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; :: 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:1;
reconsider A2 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
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 1;
A4: L[01] (((#) ((- 1),1)),(((- 1),1) (#))) is being_homeomorphism by TREAL_1:17;
reconsider hh = h as Function of (Closed-Interval-TSpace (0,1)),((TOP-REAL 2) | A2) by TOPMETR:20;
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:11;
then A6: A1 is closed by TSEP_1:12;
hh " is continuous by A3, TOPMETR:20, 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:23;
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:20; :: thesis: R | A = id A
A8: the carrier of ((TOP-REAL 2) | A2) = A1 by PRE_TOPC:8;
A9: dom R = the carrier of (Tdisk (p,r)) by FUNCT_2:def 1;
A10: dom (id A) = A ;

now :: thesis: for a being object st a in dom (R | A) holds
(R | A) . a = (id A) . a

let a be object ; :: thesis: ( a in dom (R | A) implies (R | A) . a = (id A) . a )
assume A11: a in dom (R | A) ; :: thesis: (R | A) . a = (id A) . a
then A12: a in dom R by RELAT_1:57;
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:36
.= (hh * (((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ") * (L[01] (((#) ((- 1),1)),(((- 1),1) (#)))))) * (hh ") by RELAT_1:36
.= (hh * (id (Closed-Interval-TSpace (0,1)))) * (hh ") by A4, GRCAT_1:41
.= hh * (hh ") by FUNCT_2:17
.= id ((TOP-REAL 2) | A2) by A3, GRCAT_1:41 ;
thus (R | A) . a = R . a by A11, FUNCT_1:49
.= (hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) . (g . a) by A13, A12, FUNCT_1:13
.= (hh * ((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) ")) . (((L[01] (((#) ((- 1),1)),(((- 1),1) (#)))) * (hh ")) . a) by A7, A11, FUNCT_1:49
.= (id A) . a by A8, A11, A14, A15, FUNCT_1:13 ; :: thesis: verum

end;

hence R | A = id A by A2, A9, A10, FUNCT_1:2, RELAT_1:62; :: thesis: verum