let C be Simple_closed_curve; :: thesis: for h being Homeomorphism of TOP-REAL 2 holds h .: C is being_simple_closed_curve
let h be Homeomorphism of TOP-REAL 2; :: thesis: h .: C is being_simple_closed_curve
consider f being Function of ((TOP-REAL 2) | R^2-unit_square),((TOP-REAL 2) | C) such that
A1: f is being_homeomorphism by TOPREAL2:def 1;
reconsider g = h | C as Function of ((TOP-REAL 2) | C),((TOP-REAL 2) | (h .: C)) by JORDAN24:12;
take g * f ; :: according to TOPREAL2:def 1 :: thesis: g * f is being_homeomorphism
g is being_homeomorphism by JORDAN24:14;
hence g * f is being_homeomorphism by A1, TOPS_2:57; :: thesis: verum