let q1, q2 be Point of (TOP-REAL 2); :: thesis: for Q, P being non empty Subset of (TOP-REAL 2)
for f being Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
let Q, P be non empty Subset of (TOP-REAL 2); :: thesis: for f being Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
let f be Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P); :: thesis: ( f is being_homeomorphism & Q is_an_arc_of q1,q2 implies for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2 )
assume that
A1: f is being_homeomorphism and
A2: Q is_an_arc_of q1,q2 ; :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1 = f . q1 & p2 = f . q2 implies P is_an_arc_of p1,p2 )
assume A3: ( p1 = f . q1 & p2 = f . q2 ) ; :: thesis: P is_an_arc_of p1,p2
reconsider f = f as Function of ((TOP-REAL 2) | Q),((TOP-REAL 2) | P) ;
consider f1 being Function of I[01] ,((TOP-REAL 2) | Q) such that
A4: ( f1 is being_homeomorphism & f1 . 0 = q1 & f1 . 1 = q2 ) by A2, TOPREAL1:def 2;
set g1 = f * f1;
A5: f * f1 is being_homeomorphism by A1, A4, TOPS_2:71;
A6: ( dom f1 = the carrier of I[01] & the carrier of I[01] = [.0 ,1.] ) by BORSUK_1:83, FUNCT_2:def 1;
then 0 in dom f1 by XXREAL_1:1;
then A7: (f * f1) . 0 = p1 by A3, A4, FUNCT_1:23;
1 in dom f1 by A6, XXREAL_1:1;
then (f * f1) . 1 = p2 by A3, A4, FUNCT_1:23;
hence P is_an_arc_of p1,p2 by A5, A7, TOPREAL1:def 2; :: thesis: verum