A1: 0 = (#) 0 ,1 by TREAL_1:def 1;
let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n)
for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
let A be Subset of (TOP-REAL n); :: thesis: for p, q being Point of (TOP-REAL n)
for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
let p, q be Point of (TOP-REAL n); :: thesis: for a, b being Point of I[01] st A is_an_arc_of p,q & a < b holds
ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
let a, b be Point of I[01] ; :: thesis: ( A is_an_arc_of p,q & a < b implies ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q ) )
assume that
A2: A is_an_arc_of p,q and
A3: a < b ; :: thesis: ex E being non empty Subset of I[01] ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
reconsider E = [.a,b.] as non empty Subset of I[01] by A3, Th49;
A4: b <= 1 by BORSUK_1:86;
0 <= a by BORSUK_1:86;
then A5: I[01] | E = Closed-Interval-TSpace a,b by A3, A4, TOPMETR:31;
then reconsider e = P[01] a,b,((#) 0 ,1),(0 ,1 (#) ) as Function of (I[01] | E),I[01] by TOPMETR:27;
take E ; :: thesis: ex f being Function of (I[01] | E),((TOP-REAL n) | A) st
( E = [.a,b.] & f is being_homeomorphism & f . a = p & f . b = q )
A6: a = (#) a,b by A3, TREAL_1:def 1;
reconsider B = A as non empty Subset of (TOP-REAL n) by A2, TOPREAL1:4;
consider f being Function of I[01] ,((TOP-REAL n) | B) such that
A7: f is being_homeomorphism and
A8: f . 0 = p and
A9: f . 1 = q by A2, TOPREAL1:def 2;
set g = f * e;
reconsider g = f * e as Function of (I[01] | E),((TOP-REAL n) | A) ;
take g ; :: thesis: ( E = [.a,b.] & g is being_homeomorphism & g . a = p & g . b = q )
thus E = [.a,b.] ; :: thesis: ( g is being_homeomorphism & g . a = p & g . b = q )
e is being_homeomorphism by A3, A5, TOPMETR:27, TREAL_1:20;
hence g is being_homeomorphism by A7, TOPS_2:71; :: thesis: ( g . a = p & g . b = q )
a in E by A3, XXREAL_1:1;
then a in the carrier of (I[01] | E) by PRE_TOPC:29;
hence g . a = f . (e . a) by FUNCT_2:21
.= p by A3, A8, A1, A6, TREAL_1:16 ;
:: thesis: g . b = q
A10: 1 = 0 ,1 (#) by TREAL_1:def 2;
A11: b = a,b (#) by A3, TREAL_1:def 2;
b in E by A3, XXREAL_1:1;
then b in the carrier of (I[01] | E) by PRE_TOPC:29;
hence g . b = f . (e . b) by FUNCT_2:21
.= q by A3, A9, A10, A11, TREAL_1:16 ;
:: thesis: verum