let T1, T2 be TopSpace; :: thesis: for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
let A2 be Subset of T2; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism )
assume A1: f is being_homeomorphism ; :: thesis: for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
A2: ( dom f = [#] T1 & rng f = [#] T2 ) by A1, TOPS_2:def 5;
T1,T2 are_homeomorphic by A1, T_0TOPSP:def 1;
then ( T1 is empty iff T2 is empty ) by YELLOW14:18;
then A3: ( [#] T1 = {} iff [#] T2 = {} ) ;
A4: rng f = [#] T2 by A1, TOPS_2:def 5;
set A = f " A2;
let g be Function of (T1 | (f " A2)),(T2 | A2); :: thesis: ( g = A2 |` f implies g is being_homeomorphism )
assume A5: g = A2 |` f ; :: thesis: g is being_homeomorphism
A6: rng g = A2 by A2, A5, RELAT_1:89;
A7: f is one-to-one by A1, TOPS_2:def 5;
then A8: g is one-to-one by A5, FUNCT_1:58;
set TA = T1 | (f " A2);
set TB = T2 | A2;
A10: [#] (T1 | (f " A2)) = f " A2 by PRE_TOPC:def 5;
A11: ( [#] (T1 | (f " A2)) = {} iff [#] (T2 | A2) = {} ) by A6;
A12: [#] (T2 | A2) = A2 by PRE_TOPC:def 5;
A13: f is continuous by A1, TOPS_2:def 5;
for P being Subset of (T2 | A2) st P is open holds
g " P is open

proof

let P be Subset of (T2 | A2); :: thesis: ( P is open implies g " P is open )
assume P is open ; :: thesis: g " P is open
then consider P1 being Subset of T2 such that
A14: P1 is open and
A15: P = P1 /\ A2 by A12, TSP_1:def 1;
A16: f " P1 is open by A3, A13, A14, TOPS_2:43;
g " P = f " P by A5, Th2, A15, XBOOLE_1:17
.= (f " P1) /\ the carrier of (T1 | (f " A2)) by A10, A15, FUNCT_1:68 ;
hence g " P is open by A16, TSP_1:def 1; :: thesis: verum

end;

then A17: g is continuous by A11, TOPS_2:43;
A18: f " is continuous by A1, TOPS_2:def 5;
for P being Subset of (T1 | (f " A2)) st P is open holds
(g ") " P is open

proof

let P be Subset of (T1 | (f " A2)); :: thesis: ( P is open implies (g ") " P is open )
assume P is open ; :: thesis: (g ") " P is open
then consider P1 being Subset of T1 such that
A19: P1 is open and
A20: P = P1 /\ (f " A2) by A10, TSP_1:def 1;
A21: (f ") " P1 is open by A3, A18, A19, TOPS_2:43;
A2 = f .: (f " A2) by A2, FUNCT_1:77;
then A22: the carrier of (T2 | A2) = (f ") " (f " A2) by A12, A4, A7, TOPS_2:54;
(g ") " P = (A2 |` f) .: P by A5, A6, A8, A12, TOPS_2:54
.= (f .: P) /\ the carrier of (T2 | A2) by A12, FUNCT_1:67
.= ((f ") " (P1 /\ (f " A2))) /\ the carrier of (T2 | A2) by A4, A7, A20, TOPS_2:54
.= (((f ") " P1) /\ ((f ") " (f " A2))) /\ the carrier of (T2 | A2) by FUNCT_1:68
.= ((f ") " P1) /\ (((f ") " (f " A2)) /\ the carrier of (T2 | A2)) by XBOOLE_1:16
.= ((f ") " P1) /\ the carrier of (T2 | A2) by A22 ;
hence (g ") " P is open by A21, TSP_1:def 1; :: thesis: verum

end;

then g " is continuous by A11, TOPS_2:43;
hence g is being_homeomorphism by A6, A5, Th1, A10, A8, A12, A17, TOPS_2:def 5; :: thesis: verum