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, Th21;
A4: b <= 1 by BORSUK_1:43;
0 <= a by BORSUK_1:43;
then A5: I[01] | E = Closed-Interval-TSpace (a,b) by A3, A4, TOPMETR:24;
then reconsider e = P[01] (a,b,((#) (0,1)),((0,1) (#))) as Function of (I[01] | E),I[01] by TOPMETR:20;
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:1;
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 1;
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:20, TREAL_1:17;
hence g is being_homeomorphism by A7, TOPS_2:57; :: 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:8;
hence g . a = f . (e . a) by FUNCT_2:15
.= p by A3, A8, A1, A6, TREAL_1:13 ;
:: 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:8;
hence g . b = f . (e . b) by FUNCT_2:15
.= q by A3, A9, A10, A11, TREAL_1:13 ;
:: thesis: verum