let S1, T1, S2, T2 be TopSpace; :: thesis: for f being Function of S1,S2
for g being Function of T1,T2 st TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of T1,the topology of T1 #) & TopStruct(# the carrier of S2,the topology of S2 #) = TopStruct(# the carrier of T2,the topology of T2 #) & f = g & f is continuous holds
g is continuous
let f be Function of S1,S2; :: thesis: for g being Function of T1,T2 st TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of T1,the topology of T1 #) & TopStruct(# the carrier of S2,the topology of S2 #) = TopStruct(# the carrier of T2,the topology of T2 #) & f = g & f is continuous holds
g is continuous
let g be Function of T1,T2; :: thesis: ( TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of T1,the topology of T1 #) & TopStruct(# the carrier of S2,the topology of S2 #) = TopStruct(# the carrier of T2,the topology of T2 #) & f = g & f is continuous implies g is continuous )
assume that
A1: TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of T1,the topology of T1 #) and
A2: TopStruct(# the carrier of S2,the topology of S2 #) = TopStruct(# the carrier of T2,the topology of T2 #) and
A3: ( f = g & f is continuous ) ; :: thesis: g is continuous

now

let P2 be Subset of T2; :: thesis: ( P2 is closed implies g " P2 is closed )
assume A4: P2 is closed ; :: thesis: g " P2 is closed
reconsider P1 = P2 as Subset of S2 by A2;
P1 is closed by A2, A4, TOPS_3:79;
then f " P1 is closed by A3, PRE_TOPC:def 12;
hence g " P2 is closed by A1, A3, TOPS_3:79; :: thesis: verum

end;

hence g is continuous by PRE_TOPC:def 12; :: thesis: verum