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

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