let S, T be TopSpace; for f being Function of S,T
for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let f be Function of S,T; for g being Function of S,TopStruct(# the carrier of T, the topology of T #) st f = g holds
( f is continuous iff g is continuous )
let g be Function of S,TopStruct(# the carrier of T, the topology of T #); ( f = g implies ( f is continuous iff g is continuous ) )
assume A1:
f = g
; ( f is continuous iff g is continuous )
thus
( f is continuous implies g is continuous )
by Th31, A1; ( g is continuous implies f is continuous )
assume A2:
g is continuous
; f is continuous
let P1 be Subset of T; PRE_TOPC:def 6 ( P1 is closed implies f " P1 is closed )
reconsider P = P1 as Subset of TopStruct(# the carrier of T, the topology of T #) ;
assume
P1 is closed
; f " P1 is closed
then
P is closed
by Th31;
hence
f " P1 is closed
by A1, A2; verum