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

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