let P, Q be Subset of (TOP-REAL 2); ( 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
; 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; verum