let T1, T2 be TopSpace; :: thesis: for A1 being Subset of T1
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
let A1 be Subset of T1; :: thesis: for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
let f be Function of T1,T2; :: thesis: ( f is being_homeomorphism implies for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism )
assume A1: f is being_homeomorphism ; :: thesis: for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
A2: dom f = [#] T1 by A1;
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;
set B = f .: A1;
let g be Function of (T1 | A1),(T2 | (f .: A1)); :: thesis: ( g = f | A1 implies g is being_homeomorphism )
assume A5: g = f | A1 ; :: thesis: g is being_homeomorphism
A6: rng g = f .: A1 by A5, RELAT_1:115;
A7: f is one-to-one by A1;
then A8: g is one-to-one by A5, FUNCT_1:52;
A9: dom g = (dom f) /\ A1 by A5, RELAT_1:61
.= A1 by A2, XBOOLE_1:28 ;
set TA = T1 | A1;
set TB = T2 | (f .: A1);
A10: [#] (T1 | A1) = A1 by PRE_TOPC:def 5;
A11: ( [#] (T1 | A1) = {} iff [#] (T2 | (f .: A1)) = {} ) by A9;
A12: [#] (T2 | (f .: A1)) = f .: A1 by PRE_TOPC:def 5;
A13: f is continuous by A1;
for P being Subset of (T2 | (f .: A1)) st P is open holds
g " P is open

proof

let P be Subset of (T2 | (f .: A1)); :: 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 /\ (f .: A1) by A12, TSP_1:def 1;
reconsider PA = (f " P1) /\ A1 as Subset of (T1 | A1) by A10, XBOOLE_1:17;
A1 = f " (f .: A1) by A2, A7, FUNCT_1:94;
then ( A1 /\ PA = PA & PA = f " P ) by A15, FUNCT_1:68, XBOOLE_1:17, XBOOLE_1:28;
then A16: g " P = PA by A5, FUNCT_1:70;
f " P1 is open by A3, A13, A14, TOPS_2:43;
hence g " P is open by A10, A16, TSP_1:def 1; :: thesis: verum

end;

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

proof

let P be Subset of (T1 | A1); :: 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 /\ A1 by A10, TSP_1:def 1;
reconsider PB = ((f ") " P1) /\ (f .: A1) as Subset of (T2 | (f .: A1)) by A12, XBOOLE_1:17;
A21: (f ") " P1 is open by A3, A18, A19, TOPS_2:43;
f .: A1 = (f ") " A1 by A4, A7, TOPS_2:54;
then PB = (f ") " (P1 /\ A1) by FUNCT_1:68
.= f .: P by A4, A7, A20, TOPS_2:54
.= g .: P by A5, A10, RELAT_1:129
.= (g ") " P by A6, A8, A12, TOPS_2:54 ;
hence (g ") " P is open by A12, A21, TSP_1:def 1; :: thesis: verum

end;

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