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

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

let g be Function of I,(); :: thesis: ( g is continuous & g is one-to-one & rng g = P implies ex f being Function of I,(() | 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,(() | P) st
( f = g & f is being_homeomorphism )

the carrier of (() | P) = [#] (() | P) ;
then A3: the carrier of (() | P) = P by PRE_TOPC:def 5;
then reconsider f = g as Function of I,(() | P) by ;
take f ; :: thesis: ( f = g & f is being_homeomorphism )
thus f = g ; :: thesis:
A4: [#] (() | P) = P by PRE_TOPC:def 5;
A5: dom f = the carrier of I by FUNCT_2:def 1
.= [#] I ;
A6: [#] () <> {} ;
for P2 being Subset of (() | P) st P2 is open holds
f " P2 is open
proof
let P2 be Subset of (() | 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 () such that
A7: C is open and
A8: C /\ ([#] (() | P)) = P2 by TOPS_2:24;
g " P = [#] I by ;
then f " P2 = (f " C) /\ () by
.= f " C by XBOOLE_1:28 ;
hence f " P2 is open by ; :: thesis: verum
end;
then A9: f is continuous by ;
rng f = [#] (() | P) by ;
hence f is being_homeomorphism by ; :: thesis: verum