let S, T be TopSpace; :: thesis: 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; :: thesis: 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 #); :: thesis: ( f = g implies ( f is continuous iff g is continuous ) )
assume Z0: f = g ; :: thesis: ( f is continuous iff g is continuous )
thus ( f is continuous implies g is continuous ) :: thesis: ( g is continuous implies f is continuous )

proof

assume Z: f is continuous ; :: thesis: g is continuous
let P1 be Subset of TopStruct(# the carrier of T,the topology of T #); :: according to PRE_TOPC:def 12 :: thesis: ( P1 is closed implies g " P1 is closed )
reconsider P = P1 as Subset of T ;
assume P1 is closed ; :: thesis: g " P1 is closed
then P is closed by Th60;
then f " P is closed by Z, Def12;
hence g " P1 is closed by Z0; :: thesis: verum

end;

assume Z: g is continuous ; :: thesis: f is continuous
let P1 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( 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 ; :: thesis: f " P1 is closed
then P is closed by Th60;
then g " P is closed by Z, Def12;
hence f " P1 is closed by Z0; :: thesis: verum