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

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

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

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

then A17:
g is continuous
by A11, TOPS_2:43;
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;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

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

then
g " is continuous
by A11, TOPS_2:43;
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;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

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