let n be Nat; :: thesis: for P being non empty Subset of ()
for f being Function of I,(() | P) st f is being_homeomorphism holds
ex g being Function of I,() st
( f = g & g is continuous & g is one-to-one )

let P be non empty Subset of (); :: thesis: for f being Function of I,(() | P) st f is being_homeomorphism holds
ex g being Function of I,() st
( f = g & g is continuous & g is one-to-one )

let f be Function of I,(() | P); :: thesis: ( f is being_homeomorphism implies ex g being Function of I,() st
( f = g & g is continuous & g is one-to-one ) )

A1: [#] (() | P) = P by PRE_TOPC:def 5;
the carrier of (() | P) = [#] (() | P)
.= P by PRE_TOPC:def 5 ;
then reconsider g1 = f as Function of I,() by FUNCT_2:7;
assume A2: f is being_homeomorphism ; :: thesis: ex g being Function of I,() st
( f = g & g is continuous & g is one-to-one )

then A3: f is one-to-one by TOPS_2:def 5;
A4: ( [#] (() | P) <> {} & f is continuous ) by ;
A5: for P2 being Subset of () st P2 is open holds
g1 " P2 is open
proof
let P2 be Subset of (); :: thesis: ( P2 is open implies g1 " P2 is open )
reconsider B1 = P2 /\ P as Subset of (() | P) by ;
f " (rng f) c= f " P by ;
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 ;
then A7: f " B1 is open by ;
f " P c= dom f by RELAT_1:132;
then ( f " B1 = (f " P2) /\ (f " P) & f " P = dom f ) by ;
hence g1 " P2 is open by ; :: thesis: verum
end;
[#] () <> {} ;
then g1 is continuous by ;
hence ex g being Function of I,() st
( f = g & g is continuous & g is one-to-one ) by A3; :: thesis: verum