let n be Nat; :: thesis: for P being non empty Subset of (TOP-REAL n)

for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds

ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism )

let P be non empty Subset of (TOP-REAL n); :: thesis: for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds

ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism )

let g be Function of I[01],(TOP-REAL n); :: thesis: ( g is continuous & g is one-to-one & rng g = P implies ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism ) )

assume that

A1: ( g is continuous & g is one-to-one ) and

A2: rng g = P ; :: thesis: ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism )

the carrier of ((TOP-REAL n) | P) = [#] ((TOP-REAL n) | P) ;

then A3: the carrier of ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

then reconsider f = g as Function of I[01],((TOP-REAL n) | P) by A2, FUNCT_2:6;

take f ; :: thesis: ( f = g & f is being_homeomorphism )

thus f = g ; :: thesis: f is being_homeomorphism

A4: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

A5: dom f = the carrier of I[01] by FUNCT_2:def 1

.= [#] I[01] ;

A6: [#] (TOP-REAL n) <> {} ;

for P2 being Subset of ((TOP-REAL n) | P) st P2 is open holds

f " P2 is open

rng f = [#] ((TOP-REAL n) | P) by A2, PRE_TOPC:def 5;

hence f is being_homeomorphism by A1, A9, COMPTS_1:17; :: thesis: verum

for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds

ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism )

let P be non empty Subset of (TOP-REAL n); :: thesis: for g being Function of I[01],(TOP-REAL n) st g is continuous & g is one-to-one & rng g = P holds

ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism )

let g be Function of I[01],(TOP-REAL n); :: thesis: ( g is continuous & g is one-to-one & rng g = P implies ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism ) )

assume that

A1: ( g is continuous & g is one-to-one ) and

A2: rng g = P ; :: thesis: ex f being Function of I[01],((TOP-REAL n) | P) st

( f = g & f is being_homeomorphism )

the carrier of ((TOP-REAL n) | P) = [#] ((TOP-REAL n) | P) ;

then A3: the carrier of ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

then reconsider f = g as Function of I[01],((TOP-REAL n) | P) by A2, FUNCT_2:6;

take f ; :: thesis: ( f = g & f is being_homeomorphism )

thus f = g ; :: thesis: f is being_homeomorphism

A4: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 5;

A5: dom f = the carrier of I[01] by FUNCT_2:def 1

.= [#] I[01] ;

A6: [#] (TOP-REAL n) <> {} ;

for P2 being Subset of ((TOP-REAL n) | P) st P2 is open holds

f " P2 is open

proof

then A9:
f is continuous
by A4, TOPS_2:43;
let P2 be Subset of ((TOP-REAL n) | P); :: thesis: ( P2 is open implies f " P2 is open )

assume P2 is open ; :: thesis: f " P2 is open

then consider C being Subset of (TOP-REAL n) such that

A7: C is open and

A8: C /\ ([#] ((TOP-REAL n) | P)) = P2 by TOPS_2:24;

g " P = [#] I[01] by A3, A5, RELSET_1:22;

then f " P2 = (f " C) /\ ([#] I[01]) by A4, A8, FUNCT_1:68

.= f " C by XBOOLE_1:28 ;

hence f " P2 is open by A1, A6, A7, TOPS_2:43; :: thesis: verum

end;assume P2 is open ; :: thesis: f " P2 is open

then consider C being Subset of (TOP-REAL n) such that

A7: C is open and

A8: C /\ ([#] ((TOP-REAL n) | P)) = P2 by TOPS_2:24;

g " P = [#] I[01] by A3, A5, RELSET_1:22;

then f " P2 = (f " C) /\ ([#] I[01]) by A4, A8, FUNCT_1:68

.= f " C by XBOOLE_1:28 ;

hence f " P2 is open by A1, A6, A7, TOPS_2:43; :: thesis: verum

rng f = [#] ((TOP-REAL n) | P) by A2, PRE_TOPC:def 5;

hence f is being_homeomorphism by A1, A9, COMPTS_1:17; :: thesis: verum