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 and
A2: rng f = [#] T2 and
A3: f is one-to-one and
A4: f is continuous and
A5: 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
f is onto by A2;
then A6: f " = f " by A3, TOPS_2:def 4;
then A7: (f ") .: (f .: A) = f " (f .: A) by A3, FUNCT_1:85
.= A by A1, A3, FUNCT_1:94 ;
A8: dom f = the carrier of T1 by FUNCT_2:def 1;
let g be Function of (T1 | A),(T2 | (f .: A)); :: thesis: ( g = f | A implies g is being_homeomorphism )
assume A9: g = f | A ; :: thesis: g is being_homeomorphism
( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def 5;
hence A10: ( dom g = [#] (T1 | A) & rng g = [#] (T2 | (f .: A)) ) by A9, A8, RELAT_1:62, RELAT_1:115; :: according to TOPS_2:def 5 :: thesis: ( g is one-to-one & g is continuous & g " is continuous )
A11: g is onto by A10;
thus g is one-to-one by A3, A9, FUNCT_1:52; :: thesis: ( g is continuous & g " is continuous )
then A12: g " = g " by A11, TOPS_2:def 4;
thus g is continuous by A4, A9, Th13; :: thesis: g " is continuous
g " = (f ") | (f .: A) by A3, A9, A6, A12, RFUNCT_2:17;
hence g " is continuous by A5, A7, Th13; :: thesis: verum