let A, B, S, T be TopSpace; :: thesis: for f being Function of A,S
for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds
g is open
let f be Function of A,S; :: thesis: for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds
g is open
let g be Function of B,T; :: thesis: ( TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open implies g is open )
assume that
A1: TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) and
A2: TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) and
A3: f = g and
A4: f is open ; :: thesis: g is open
let b be Subset of B; :: according to T_0TOPSP:def 2 :: thesis: ( not b is open or g .: b is open )
assume A5: b is open ; :: thesis: g .: b is open
reconsider a = b as Subset of A by A1;
a is open by A1, A5, TOPS_3:76;
then f .: a is open by A4;
hence g .: b is open by A2, A3, TOPS_3:76; :: thesis: verum