let n be Element of NAT ; :: thesis: for P being non empty Subset of (TOP-REAL n)
for f being Function of I[01] ,((TOP-REAL n) | P) st P <> {} & 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 P <> {} & 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: ( P <> {} & 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 ) )
assume A1: ( P <> {} & 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 )
the carrier of ((TOP-REAL n) | P) = [#] ((TOP-REAL n) | P)
.= P by PRE_TOPC:def 10 ;
then reconsider g1 = f as Function of I[01] ,(TOP-REAL n) by FUNCT_2:9;
A2: ( [#] (TOP-REAL n) <> {} & [#] ((TOP-REAL n) | P) <> {} ) ;
A4: [#] ((TOP-REAL n) | P) = P by PRE_TOPC:def 10;
A5: ( f is one-to-one & f is continuous & f " is continuous ) by A1, TOPS_2:def 5;
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 )
assume A6: P2 is open ; :: thesis: g1 " P2 is open
reconsider B1 = P2 /\ P as Subset of ((TOP-REAL n) | P) by A4, XBOOLE_1:17;
B1 is open by A4, A6, TOPS_2:32;
then A7: f " B1 is open by A2, A5, TOPS_2:55;
A8: f " B1 = (f " P2) /\ (f " P) by FUNCT_1:137;
f " (rng f) c= f " P by A4, RELAT_1:178;
then A9: dom f c= f " P by RELAT_1:169;
f " P c= dom f by RELAT_1:167;
then f " P = dom f by A9, XBOOLE_0:def 10;
hence g1 " P2 is open by A7, A8, RELAT_1:167, XBOOLE_1:28; :: thesis: verum

end;

then g1 is continuous by A2, TOPS_2:55;
hence ex g being Function of I[01] ,(TOP-REAL n) st
( f = g & g is continuous & g is one-to-one ) by A5; :: thesis: verum