let S, T be TopSpace; :: thesis: for f being Function of S,T
for g being Function of TopStruct(# the carrier of S,the topology 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 TopStruct(# the carrier of S,the topology 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 TopStruct(# the carrier of S,the topology 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 )
reconsider h = f as Function of S,TopStruct(# the carrier of T,the topology of T #) ;
( h is continuous iff g is continuous ) by Z0, Th62;
hence ( f is continuous iff g is continuous ) by Th63; :: thesis: verum