let T1, T2 be non empty TopSpace; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is being_homeomorphism
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is being_homeomorphism )
assume that
A1: ( dom f = [#] T1 & rng f = [#] T2 & f is one-to-one ) and
A2: ( f is continuous & f " is continuous ) ; :: according to TOPS_2:def 5 :: thesis: for A being Subset of T1
for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is being_homeomorphism
let A be Subset of T1; :: thesis: for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds
g is being_homeomorphism
let g be Function of (T1 | A),(T2 | (f .: A)); :: thesis: ( g = f | A implies g is being_homeomorphism )
assume A3: g = f | A ; :: thesis: g is being_homeomorphism
A4: ( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def 10;
dom f = the carrier of T1 by FUNCT_2:def 1;
hence A5: ( dom g = [#] (T1 | A) & rng g = [#] (T2 | (f .: A)) ) by A3, A4, RELAT_1:91, RELAT_1:148; :: according to TOPS_2:def 5 :: thesis: ( g is one-to-one & g is continuous & g " is continuous )
thus A6: g is one-to-one by A1, A3, FUNCT_1:84; :: thesis: ( g is continuous & g " is continuous )
thus g is continuous by A2, A3, Th13; :: thesis: g " is continuous
A7: ( f " = f " & g " = g " ) by A1, A5, A6, TOPS_2:def 4;
then A8: g " = (f " ) | (f .: A) by A1, A3, RFUNCT_2:40;
A9: (f " ) .: (f .: A) = f " (f .: A) by A1, A7, FUNCT_1:155
.= A by A1, FUNCT_1:164 ;
thus g " is continuous by A2, A8, A9, Th13; :: thesis: verum