let T1, T2 be non empty TopSpace; 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; ( 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
; TOPS_2:def 5 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; 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)); ( g = f | A implies g is being_homeomorphism )
assume A9:
g = f | A
; 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; TOPS_2:def 5 ( 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; ( g is continuous & g " is continuous )
then A12:
g " = g "
by A11, TOPS_2:def 4;
thus
g is continuous
by A4, A9, Th13; g " is continuous
g " = (f ") | (f .: A)
by A3, A9, A6, A12, RFUNCT_2:17;
hence
g " is continuous
by A5, A7, Th13; verum