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 ;
hence R | A = id A by A2, A9, A10, FUNCT_1:2, RELAT_1:62; :: thesis: verum