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 ;
T1,T2 are_homeomorphic by ;
then ( T1 is empty iff T2 is empty ) by YELLOW14:18;
then A3: ( [#] T1 = {} iff [#] T2 = {} ) ;
A4: rng f = [#] T2 by ;
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:
A6: rng g = A2 by ;
A7: f is one-to-one by ;
then A8: g is one-to-one by ;
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 ;
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 ;
A16: f " P1 is open by ;
g " P = f " P by
.= (f " P1) /\ the carrier of (T1 | (f " A2)) by ;
hence g " P is open by ; :: thesis: verum
end;
then A17: g is continuous by ;
A18: f " is continuous by ;
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 ;
A21: (f ") " P1 is open by ;
A2 = f .: (f " A2) by ;
then A22: the carrier of (T2 | A2) = (f ") " (f " A2) by ;
(g ") " P = (A2 |` f) .: P by
.= (f .: P) /\ the carrier of (T2 | A2) by
.= ((f ") " (P1 /\ (f " A2))) /\ the carrier of (T2 | A2) by
.= (((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 ; :: thesis: verum
end;
then g " is continuous by ;
hence g is being_homeomorphism by ; :: thesis: verum