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

proof

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;

[#] (TOP-REAL n) <> {} ;
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