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 1;

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:40, XXREAL_1:1;

then A9: (f * f1) . 0 = p1 by A3, A6, FUNCT_1:13;

1 in dom f1 by A8, BORSUK_1:40, XXREAL_1:1;

then A10: (f * f1) . 1 = p2 by A4, A7, FUNCT_1:13;

f * f1 is being_homeomorphism by A1, A5, TOPS_2:57;

hence P is_an_arc_of p1,p2 by A9, A10, TOPREAL1:def 1; :: thesis: verum

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 1;

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:40, XXREAL_1:1;

then A9: (f * f1) . 0 = p1 by A3, A6, FUNCT_1:13;

1 in dom f1 by A8, BORSUK_1:40, XXREAL_1:1;

then A10: (f * f1) . 1 = p2 by A4, A7, FUNCT_1:13;

f * f1 is being_homeomorphism by A1, A5, TOPS_2:57;

hence P is_an_arc_of p1,p2 by A9, A10, TOPREAL1:def 1; :: thesis: verum