let P, Q be Subset of (TOP-REAL 2); :: thesis: ( ex f being Function of ((TOP-REAL 2) | P),((TOP-REAL 2) | 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 ((TOP-REAL 2) | P),((TOP-REAL 2) | Q) st f is being_homeomorphism and
A2: P is being_simple_closed_curve ; :: thesis: Q is being_simple_closed_curve
consider f being Function of ((TOP-REAL 2) | P),((TOP-REAL 2) | Q) such that
A3: f is being_homeomorphism by A1;
consider g being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P) such that
A4: g is being_homeomorphism by A2, TOPREAL2:def 1;
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 A5, TOPREAL1:14;
A7: dom g = [#] ((TOP-REAL 2) | R^2-unit_square) by A4, TOPS_2:def 5;
A8: rng g = [#] ((TOP-REAL 2) | P) by A4, TOPS_2:def 5;
dom g = R^2-unit_square by A7, PRE_TOPC:def 5;
then A9: g . |[1,0]| in rng g by A6, FUNCT_1:3;
then A10: g . |[1,0]| in P by A8, PRE_TOPC:def 5;
reconsider P1 = P as non empty Subset of (TOP-REAL 2) by A9;
dom f = [#] ((TOP-REAL 2) | P) by A3, TOPS_2:def 5;
then dom f = P by PRE_TOPC:def 5;
then f . (g . |[1,0]|) in rng f by A10, FUNCT_1:3;
then reconsider Q1 = Q as non empty Subset of (TOP-REAL 2) ;
reconsider f1 = f as Function of ((TOP-REAL 2) | P1),((TOP-REAL 2) | Q1) ;
reconsider g1 = g as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | P1) ;
reconsider h = f1 * g1 as Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | Q1) ;
h is being_homeomorphism by A3, A4, TOPS_2:57;
hence Q is being_simple_closed_curve by TOPREAL2:def 1; :: thesis: verum