let X, Y, Z be non empty TopSpace; :: thesis: ( the carrier of X = the carrier of Y & the topology of Y c= the topology of X implies for f being Function of X,Z

for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x )

assume that

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

A2: the topology of Y c= the topology of X ; :: thesis: for f being Function of X,Z

for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let f be Function of X,Z; :: thesis: for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let g be Function of Y,Z; :: thesis: ( f = g implies for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x )

assume A3: f = g ; :: thesis: for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let x be Point of X; :: thesis: for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let y be Point of Y; :: thesis: ( x = y & g is_continuous_at y implies f is_continuous_at x )

assume A4: x = y ; :: thesis: ( not g is_continuous_at y or f is_continuous_at x )

assume A5: g is_continuous_at y ; :: thesis: f is_continuous_at x

for G being Subset of Z st G is open & f . x in G holds

ex H being Subset of X st

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

for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x )

assume that

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

A2: the topology of Y c= the topology of X ; :: thesis: for f being Function of X,Z

for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let f be Function of X,Z; :: thesis: for g being Function of Y,Z st f = g holds

for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let g be Function of Y,Z; :: thesis: ( f = g implies for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x )

assume A3: f = g ; :: thesis: for x being Point of X

for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let x be Point of X; :: thesis: for y being Point of Y st x = y & g is_continuous_at y holds

f is_continuous_at x

let y be Point of Y; :: thesis: ( x = y & g is_continuous_at y implies f is_continuous_at x )

assume A4: x = y ; :: thesis: ( not g is_continuous_at y or f is_continuous_at x )

assume A5: g is_continuous_at y ; :: thesis: f is_continuous_at x

for G being Subset of Z st G is open & f . x in G holds

ex H being Subset of X st

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

proof

hence
f is_continuous_at x
by Th43; :: thesis: verum
let G be Subset of Z; :: thesis: ( G is open & f . x in G implies ex H being Subset of X st

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

assume ( G is open & f . x in G ) ; :: thesis: ex H being Subset of X st

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

then consider H being Subset of Y such that

A6: H is open and

A7: ( y in H & g .: H c= G ) by A3, A4, A5, Th43;

reconsider F = H as Subset of X by A1;

take F ; :: thesis: ( F is open & x in F & f .: F c= G )

H in the topology of Y by A6;

hence ( F is open & x in F & f .: F c= G ) by A2, A3, A4, A7; :: thesis: verum

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

assume ( G is open & f . x in G ) ; :: thesis: ex H being Subset of X st

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

then consider H being Subset of Y such that

A6: H is open and

A7: ( y in H & g .: H c= G ) by A3, A4, A5, Th43;

reconsider F = H as Subset of X by A1;

take F ; :: thesis: ( F is open & x in F & f .: F c= G )

H in the topology of Y by A6;

hence ( F is open & x in F & f .: F c= G ) by A2, A3, A4, A7; :: thesis: verum