let A, B, S, T be TopSpace; 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; 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; ( 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
; g is open
let b be Subset of B; T_0TOPSP:def 2 ( not b is open or g .: b is open )
assume A5:
b is open
; 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; verum