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 that
A3: p1 = f . q1 and
A4: 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
A5: f1 is being_homeomorphism and
A6: f1 . 0 = q1 and
A7: f1 . 1 = q2 by A2, TOPREAL1:def 2;
set g1 = f * f1;
A8: dom f1 = the carrier of I[01] by FUNCT_2:def 1;
then 0 in dom f1 by BORSUK_1:83, XXREAL_1:1;
then A9: (f * f1) . 0 = p1 by A3, A6, FUNCT_1:23;
1 in dom f1 by A8, BORSUK_1:83, XXREAL_1:1;
then A10: (f * f1) . 1 = p2 by A4, A7, FUNCT_1:23;
f * f1 is being_homeomorphism by A1, A5, TOPS_2:71;
hence P is_an_arc_of p1,p2 by A9, A10, TOPREAL1:def 2; :: thesis: verum