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;
then A5: L[01] ((#) (- 1),1),((- 1),1 (#) ) is continuous ;
reconsider hh = h as Function of (Closed-Interval-TSpace 0 ,1),((TOP-REAL 2) | A2) by TOPMETR:27;
A6: (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 A7: A1 is closed by TSEP_1:12;
hh " is continuous by A3, TOPMETR:27, TOPS_2:def 5;
then (L[01] ((#) (- 1),1),((- 1),1 (#) )) * (hh " ) is continuous by A5;
then consider g being continuous Function of (Tdisk p,r),(Closed-Interval-TSpace (- 1),1) such that
A8: g | A1 = f by A6, A7, 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 )
A9: hh is continuous by A3, TOPMETR:27;
(L[01] ((#) (- 1),1),((- 1),1 (#) )) " is continuous by A4, TOPS_2:def 5;
then hh * ((L[01] ((#) (- 1),1),((- 1),1 (#) )) " ) is continuous by A9;
hence R is continuous ; :: thesis: R | A = id A
A10: the carrier of ((TOP-REAL 2) | A2) = A1 by PRE_TOPC:29;
dom R = the carrier of (Tdisk p,r) by FUNCT_2:def 1;
then A11: dom (R | A) = A by A2, RELAT_1:91;
A12: 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 A13: a in dom (R | A) ; :: thesis: (R | A) . a = (id A) . a
A14: dom g = the carrier of (Tdisk p,r) by FUNCT_2:def 1;
A15: dom ((L[01] ((#) (- 1),1),((- 1),1 (#) )) * (hh " )) = the carrier of ((TOP-REAL 2) | A2) by FUNCT_2:def 1;
A16: L[01] ((#) (- 1),1),((- 1),1 (#) ) is one-to-one by A4;
A17: L[01] ((#) (- 1),1),((- 1),1 (#) ) is onto by A4;
A18: ( hh is one-to-one & hh is onto ) by A3;
A19: (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 A16, A17, GRCAT_1:56
.= hh * (hh " ) by FUNCT_2:23
.= id ((TOP-REAL 2) | A2) by A18, GRCAT_1:56 ;
thus (R | A) . a = R . a by A11, A13, FUNCT_1:72
.= (hh * ((L[01] ((#) (- 1),1),((- 1),1 (#) )) " )) . (g . a) by A13, A14, FUNCT_1:23
.= (hh * ((L[01] ((#) (- 1),1),((- 1),1 (#) )) " )) . (((L[01] ((#) (- 1),1),((- 1),1 (#) )) * (hh " )) . a) by A8, A11, A13, FUNCT_1:72
.= (id A) . a by A10, A11, A13, A15, A19, FUNCT_1:23 ; :: thesis: verum

end;

hence R | A = id A by A11, A12, FUNCT_1:9; :: thesis: verum