let S, T be non empty TopSpace; :: thesis: for S0 being non empty SubSpace of S
for T0 being non empty SubSpace of T
for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
let S0 be non empty SubSpace of S; :: thesis: for T0 being non empty SubSpace of T
for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
let T0 be non empty SubSpace of T; :: thesis: for f being Function of S,T st f is being_homeomorphism holds
for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism )
assume A1: f is being_homeomorphism ; :: thesis: for g being Function of S0,T0 st g = f | S0 & g is onto holds
g is being_homeomorphism
A2: rng f = [#] T by A1;
A3: f " is continuous by A1;
let g be Function of S0,T0; :: thesis: ( g = f | S0 & g is onto implies g is being_homeomorphism )
assume that
A4: g = f | S0 and
A5: g is onto ; :: thesis: g is being_homeomorphism
A6: g = f | the carrier of S0 by A4, TMAP_1:def 4;
then A7: f .: the carrier of S0 = rng g by RELAT_1:115
.= the carrier of T0 by A5, FUNCT_2:def 3 ;
thus dom g = [#] S0 by FUNCT_2:def 1; :: according to TOPS_2:def 5 :: thesis: ( rng g = [#] T0 & g is one-to-one & g is continuous & g " is continuous )
thus rng g = [#] T0 by A5, FUNCT_2:def 3; :: thesis: ( g is one-to-one & g is continuous & g " is continuous )
A8: f is one-to-one by A1;
hence A9: g is one-to-one by A6, FUNCT_1:52; :: thesis: ( g is continuous & g " is continuous )
A10: f is onto by A2, FUNCT_2:def 3;
f is continuous by A1;
then g is continuous Function of S0,T by A4;
hence g is continuous by Th8; :: thesis: g " is continuous
g " = (f | the carrier of S0) " by A5, A6, A9, TOPS_2:def 4
.= (f ") | (f .: the carrier of S0) by A8, RFUNCT_2:17
.= (f ") | the carrier of T0 by A10, A8, A7, TOPS_2:def 4
.= (f ") | T0 by TMAP_1:def 4 ;
then g " is continuous Function of T0,S by A3;
hence g " is continuous by Th8; :: thesis: verum