let P, Q be Subset of (); :: thesis: ( ex f being Function of (() | P),(() | Q) st f is being_homeomorphism & P is being_simple_closed_curve implies Q is being_simple_closed_curve )
assume that
A1: ex f being Function of (() | P),(() | Q) st f is being_homeomorphism and
A2: P is being_simple_closed_curve ; :: thesis:
consider f being Function of (() | P),(() | Q) such that
A3: f is being_homeomorphism by A1;
consider g being Function of (),(() | P) such that
A4: g is being_homeomorphism by ;
A5: |[1,0]| `1 = 1 by EUCLID:52;
|[1,0]| `2 = 0 by EUCLID:52;
then A6: |[1,0]| in R^2-unit_square by ;
A7: dom g = [#] () by ;
A8: rng g = [#] (() | P) by ;
dom g = R^2-unit_square by ;
then A9: g . |[1,0]| in rng g by ;
then A10: g . |[1,0]| in P by ;
reconsider P1 = P as non empty Subset of () by A9;
dom f = [#] (() | P) by ;
then dom f = P by PRE_TOPC:def 5;
then f . (g . |[1,0]|) in rng f by ;
then reconsider Q1 = Q as non empty Subset of () ;
reconsider f1 = f as Function of (() | P1),(() | Q1) ;
reconsider g1 = g as Function of (),(() | P1) ;
reconsider h = f1 * g1 as Function of (),(() | Q1) ;
h is being_homeomorphism by ;
hence Q is being_simple_closed_curve by TOPREAL2:def 1; :: thesis: verum