let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for P being Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | P) st
( rng f = P & F = f )
let p1, p2 be Point of (TOP-REAL n); :: thesis: for P being Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | P) st
( rng f = P & F = f )
let P be Subset of (TOP-REAL n); :: thesis: ( P is_an_arc_of p1,p2 implies ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | P) st
( rng f = P & F = f ) )
assume A1: P is_an_arc_of p1,p2 ; :: thesis: ex F being Path of p1,p2 ex f being Function of I[01],((TOP-REAL n) | P) st
( rng f = P & F = f )
then reconsider P1 = P as non empty Subset of (TOP-REAL n) by TOPREAL1:1;
consider h being Function of I[01],((TOP-REAL n) | P) such that
A2: h is being_homeomorphism and
A3: h . 0 = p1 and
A4: h . 1 = p2 by A1, TOPREAL1:def 1;
h is Function of I[01],((TOP-REAL n) | P1) ;
then reconsider h1 = h as Function of I[01],(TOP-REAL n) by TOPREALA:7;
h1 is continuous by A2, PRE_TOPC:26;
then reconsider f = h as Path of p1,p2 by A3, A4, BORSUK_2:def 4;
take f ; :: thesis: ex f being Function of I[01],((TOP-REAL n) | P) st
( rng f = P & f = f )
take h ; :: thesis: ( rng h = P & f = h )
thus rng h = [#] ((TOP-REAL n) | P) by A2, TOPS_2:def 5
.= P by PRE_TOPC:8 ; :: thesis: f = h
thus f = h ; :: thesis: verum