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
let g be Function of S0,T0; :: thesis: ( g = f | S0 & g is onto implies g is being_homeomorphism )
assume that
A2: g = f | S0 and
A3: g is onto ; :: thesis: g is being_homeomorphism
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 A4: rng g = [#] T0 by A3, FUNCT_2:def 3; :: thesis: ( g is one-to-one & g is continuous & g " is continuous )
A5: f is one-to-one by A1, TOPS_2:def 5;
A6: g = f | the carrier of S0 by A2, TMAP_1:def 3;
hence A7: g is one-to-one by A5, FUNCT_1:84; :: thesis: ( g is continuous & g " is continuous )
f is continuous by A1, TOPS_2:def 5;
then g is continuous Function of S0,T by A2, TMAP_1:68;
hence g is continuous by Th12; :: thesis: g " is continuous
A8: rng f = [#] T by A1, TOPS_2:def 5;
A9: f .: the carrier of S0 = rng g by A6, RELAT_1:148
.= the carrier of T0 by A3, FUNCT_2:def 3 ;
A10: g " = (f | the carrier of S0) " by A4, A6, A7, TOPS_2:def 4
.= (f " ) | (f .: the carrier of S0) by A5, RFUNCT_2:40
.= (f " ) | the carrier of T0 by A5, A8, A9, TOPS_2:def 4
.= (f " ) | T0 by TMAP_1:def 3 ;
f " is continuous by A1, TOPS_2:def 5;
then g " is continuous Function of T0,S by A10, TMAP_1:68;
hence g " is continuous by Th12; :: thesis: verum