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

for f being Function of I[01],((TOP-REAL n) | P) st f is being_homeomorphism holds

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

( f = g & g is continuous & g is one-to-one )

let P be non empty Subset of (TOP-REAL n); :: thesis: for f being Function of I[01],((TOP-REAL n) | P) st f is being_homeomorphism holds

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

( f = g & g is continuous & g is one-to-one )

let f be Function of I[01],((TOP-REAL n) | P); :: thesis: ( f is being_homeomorphism implies ex g being Function of I[01],(TOP-REAL n) st

( f = g & g is continuous & g is one-to-one ) )

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

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

.= P by PRE_TOPC:def 5 ;

then reconsider g1 = f as Function of I[01],(TOP-REAL n) by FUNCT_2:7;

assume A2: f is being_homeomorphism ; :: thesis: ex g being Function of I[01],(TOP-REAL n) st

( f = g & g is continuous & g is one-to-one )

then A3: f is one-to-one by TOPS_2:def 5;

A4: ( [#] ((TOP-REAL n) | P) <> {} & f is continuous ) by A2, TOPS_2:def 5;

A5: for P2 being Subset of (TOP-REAL n) st P2 is open holds

g1 " P2 is open

then g1 is continuous by A5, TOPS_2:43;

hence ex g being Function of I[01],(TOP-REAL n) st

( f = g & g is continuous & g is one-to-one ) by A3; :: thesis: verum

for f being Function of I[01],((TOP-REAL n) | P) st f is being_homeomorphism holds

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

( f = g & g is continuous & g is one-to-one )

let P be non empty Subset of (TOP-REAL n); :: thesis: for f being Function of I[01],((TOP-REAL n) | P) st f is being_homeomorphism holds

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

( f = g & g is continuous & g is one-to-one )

let f be Function of I[01],((TOP-REAL n) | P); :: thesis: ( f is being_homeomorphism implies ex g being Function of I[01],(TOP-REAL n) st

( f = g & g is continuous & g is one-to-one ) )

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

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

.= P by PRE_TOPC:def 5 ;

then reconsider g1 = f as Function of I[01],(TOP-REAL n) by FUNCT_2:7;

assume A2: f is being_homeomorphism ; :: thesis: ex g being Function of I[01],(TOP-REAL n) st

( f = g & g is continuous & g is one-to-one )

then A3: f is one-to-one by TOPS_2:def 5;

A4: ( [#] ((TOP-REAL n) | P) <> {} & f is continuous ) by A2, TOPS_2:def 5;

A5: for P2 being Subset of (TOP-REAL n) st P2 is open holds

g1 " P2 is open

proof

[#] (TOP-REAL n) <> {}
;
let P2 be Subset of (TOP-REAL n); :: thesis: ( P2 is open implies g1 " P2 is open )

reconsider B1 = P2 /\ P as Subset of ((TOP-REAL n) | P) by A1, XBOOLE_1:17;

f " (rng f) c= f " P by A1, RELAT_1:143;

then A6: dom f c= f " P by RELAT_1:134;

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

then B1 is open by A1, TOPS_2:24;

then A7: f " B1 is open by A4, TOPS_2:43;

f " P c= dom f by RELAT_1:132;

then ( f " B1 = (f " P2) /\ (f " P) & f " P = dom f ) by A6, FUNCT_1:68;

hence g1 " P2 is open by A7, RELAT_1:132, XBOOLE_1:28; :: thesis: verum

end;reconsider B1 = P2 /\ P as Subset of ((TOP-REAL n) | P) by A1, XBOOLE_1:17;

f " (rng f) c= f " P by A1, RELAT_1:143;

then A6: dom f c= f " P by RELAT_1:134;

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

then B1 is open by A1, TOPS_2:24;

then A7: f " B1 is open by A4, TOPS_2:43;

f " P c= dom f by RELAT_1:132;

then ( f " B1 = (f " P2) /\ (f " P) & f " P = dom f ) by A6, FUNCT_1:68;

hence g1 " P2 is open by A7, RELAT_1:132, XBOOLE_1:28; :: thesis: verum

then g1 is continuous by A5, TOPS_2:43;

hence ex g being Function of I[01],(TOP-REAL n) st

( f = g & g is continuous & g is one-to-one ) by A3; :: thesis: verum