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