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 and
A4: f is continuous ; :: thesis: g is continuous
now :: thesis: for P2 being Subset of T2 st P2 is closed holds
g " P2 is closed
let P2 be Subset of T2; :: thesis: ( P2 is closed implies g " P2 is closed )
assume A5: P2 is closed ; :: thesis: g " P2 is closed
reconsider P1 = P2 as Subset of S2 by A2;
P1 is closed by A2, A5, TOPS_3:79;
then f " P1 is closed by A4;
hence g " P2 is closed by A1, A3, TOPS_3:79; :: thesis: verum
end;
hence g is continuous ; :: thesis: verum