let q1, q2 be Point of (); :: thesis: for Q, P being non empty Subset of ()
for f being Function of (() | Q),(() | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of () st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2

let Q, P be non empty Subset of (); :: thesis: for f being Function of (() | Q),(() | P) st f is being_homeomorphism & Q is_an_arc_of q1,q2 holds
for p1, p2 being Point of () st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2

let f be Function of (() | Q),(() | P); :: thesis: ( f is being_homeomorphism & Q is_an_arc_of q1,q2 implies for p1, p2 being Point of () 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 () st p1 = f . q1 & p2 = f . q2 holds
P is_an_arc_of p1,p2

let p1, p2 be Point of (); :: 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 (() | Q),(() | P) ;
consider f1 being Function of I,(() | Q) such that
A5: f1 is being_homeomorphism and
A6: f1 . 0 = q1 and
A7: f1 . 1 = q2 by ;
set g1 = f * f1;
A8: dom f1 = the carrier of I by FUNCT_2:def 1;
then 0 in dom f1 by ;
then A9: (f * f1) . 0 = p1 by ;
1 in dom f1 by ;
then A10: (f * f1) . 1 = p2 by ;
f * f1 is being_homeomorphism by ;
hence P is_an_arc_of p1,p2 by ; :: thesis: verum