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 A1: ( ex f being Function of ((TOP-REAL 2) | P),((TOP-REAL 2) | Q) st f is being_homeomorphism & P is being_simple_closed_curve ) ; :: thesis: Q is being_simple_closed_curve
then consider f being Function of ((TOP-REAL 2) | P),((TOP-REAL 2) | Q) such that
A2: f is being_homeomorphism ;
consider g being Function of ((TOP-REAL 2) | R^2-unit_square ),((TOP-REAL 2) | P) such that
A3: g is being_homeomorphism by A1, TOPREAL2:def 1;
( |[1,0 ]| `1 = 1 & |[1,0 ]| `2 = 0 ) by EUCLID:56;
then A4: |[1,0 ]| in R^2-unit_square by TOPREAL1:20;
A5: ( dom g = [#] ((TOP-REAL 2) | R^2-unit_square ) & rng g = [#] ((TOP-REAL 2) | P) ) by A3, TOPS_2:def 5;
then dom g = R^2-unit_square by PRE_TOPC:def 10;
then A6: g . |[1,0 ]| in rng g by A4, FUNCT_1:12;
then A7: g . |[1,0 ]| in P by A5, PRE_TOPC:def 10;
reconsider P1 = P as non empty Subset of (TOP-REAL 2) by A6, PRE_TOPC:def 10;
( dom f = [#] ((TOP-REAL 2) | P) & rng f = [#] ((TOP-REAL 2) | Q) ) by A2, TOPS_2:def 5;
then dom f = P by PRE_TOPC:def 10;
then f . (g . |[1,0 ]|) in rng f by A7, FUNCT_1:12;
then reconsider Q1 = Q as non empty Subset of (TOP-REAL 2) by PRE_TOPC:def 10;
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 A2, A3, TOPS_2:71;
hence Q is being_simple_closed_curve by TOPREAL2:def 1; :: thesis: verum