let X, Y, Z be non empty TopSpace; :: thesis: ( the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y implies for f being Function of X,Y
for g being Function of X,Z st f = g holds
for x being Point of X st f is_continuous_at x holds
g is_continuous_at x )
assume A1: ( the carrier of Y = the carrier of Z & the topology of Z c= the topology of Y ) ; :: thesis: for f being Function of X,Y
for g being Function of X,Z st f = g holds
for x being Point of X st f is_continuous_at x holds
g is_continuous_at x
let f be Function of X,Y; :: thesis: for g being Function of X,Z st f = g holds
for x being Point of X st f is_continuous_at x holds
g is_continuous_at x
let g be Function of X,Z; :: thesis: ( f = g implies for x being Point of X st f is_continuous_at x holds
g is_continuous_at x )
assume A2: f = g ; :: thesis: for x being Point of X st f is_continuous_at x holds
g is_continuous_at x
let x be Point of X; :: thesis: ( f is_continuous_at x implies g is_continuous_at x )
assume A3: f is_continuous_at x ; :: thesis: g is_continuous_at x
for G being Subset of Z st G is open & g . x in G holds
ex H being Subset of X st
( H is open & x in H & g .: H c= G )

proof

let G be Subset of Z; :: thesis: ( G is open & g . x in G implies ex H being Subset of X st
( H is open & x in H & g .: H c= G ) )
reconsider F = G as Subset of Y by A1;
assume A4: ( G is open & g . x in G ) ; :: thesis: ex H being Subset of X st
( H is open & x in H & g .: H c= G )
then G in the topology of Z by PRE_TOPC:def 5;
then ( f . x in F & F is open ) by A1, A2, A4, PRE_TOPC:def 5;
then consider H being Subset of X such that
A5: ( H is open & x in H & f .: H c= F ) by A3, Th48;
take H ; :: thesis: ( H is open & x in H & g .: H c= G )
thus ( H is open & x in H & g .: H c= G ) by A2, A5; :: thesis: verum

end;

hence g is_continuous_at x by Th48; :: thesis: verum