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 that

A1: the carrier of Y = the carrier of Z and

A2: 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 A3: 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 A4: 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 )

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 that

A1: the carrier of Y = the carrier of Z and

A2: 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 A3: 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 A4: 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

hence
g is_continuous_at x
by Th43; :: thesis: verum
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 that

A5: G is open and

A6: g . x in G ; :: thesis: ex H being Subset of X st

( H is open & x in H & g .: H c= G )

G in the topology of Z by A5;

then F is open by A2;

then consider H being Subset of X such that

A7: ( H is open & x in H & f .: H c= F ) by A3, A4, A6, Th43;

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 A3, A7; :: thesis: verum

end;( H is open & x in H & g .: H c= G ) )

reconsider F = G as Subset of Y by A1;

assume that

A5: G is open and

A6: g . x in G ; :: thesis: ex H being Subset of X st

( H is open & x in H & g .: H c= G )

G in the topology of Z by A5;

then F is open by A2;

then consider H being Subset of X such that

A7: ( H is open & x in H & f .: H c= F ) by A3, A4, A6, Th43;

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 A3, A7; :: thesis: verum