let S, T be non empty TopSpace; :: thesis: for S1 being Subset of S
for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let S1 be Subset of S; :: thesis: for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let T1 be Subset of T; :: thesis: for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let f be Function of S,T; :: thesis: for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let g be Function of (S | S1),(T | T1); :: thesis: ( g = f | S1 & g is onto & f is open & f is one-to-one implies g is open )
assume that
A1: g = f | S1 and
A2: rng g = the carrier of (T | T1) and
A3: f is open and
A4: f is one-to-one ; :: according to FUNCT_2:def 3 :: thesis: g is open
let A be Subset of (S | S1); :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or g .: A is open )
A5: [#] (T | T1) = T1 by PRE_TOPC:def 5;
assume A is open ; :: thesis: g .: A is open
then consider C being Subset of S such that
A6: C is open and
A7: C /\ ([#] (S | S1)) = A by TOPS_2:24;
A8: ( [#] (S | S1) = S1 & g .: (C /\ S1) c= (g .: C) /\ (g .: S1) ) by PRE_TOPC:def 5, RELAT_1:121;
A9: g .: A = (f .: C) /\ T1

proof

g .: C c= f .: C by A1, RELAT_1:128;
then (g .: C) /\ (g .: S1) c= (f .: C) /\ T1 by A5, XBOOLE_1:27;
hence g .: A c= (f .: C) /\ T1 by A7, A8; :: according to XBOOLE_0:def 10 :: thesis: (f .: C) /\ T1 c= g .: A
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (f .: C) /\ T1 or y in g .: A )
A10: ( dom g c= dom f & dom f = the carrier of S ) by A1, FUNCT_2:def 1, RELAT_1:60;
assume A11: y in (f .: C) /\ T1 ; :: thesis: y in g .: A
then y in f .: C by XBOOLE_0:def 4;
then consider x being Element of S such that
A12: x in C and
A13: y = f . x by FUNCT_2:65;
y in T1 by A11, XBOOLE_0:def 4;
then consider a being object such that
A14: a in dom g and
A15: g . a = y by A2, A5, FUNCT_1:def 3;
f . a = g . a by A1, A14, FUNCT_1:47;
then a = x by A4, A13, A14, A15, A10, FUNCT_1:def 4;
then a in A by A7, A12, A14, XBOOLE_0:def 4;
hence y in g .: A by A14, A15, FUNCT_1:def 6; :: thesis: verum

end;

f .: C is open by A3, A6;
hence g .: A is open by A5, A9, TOPS_2:24; :: thesis: verum