let X, Y, Z be non empty TopSpace; :: thesis:
assume that
A1: the carrier of X = the carrier of Y and
A2: the topology of Y c= the topology of X ; :: thesis:
let f be Function of X,Z; :: thesis:
let g be Function of Y,Z; :: thesis:
assume A3: f = g ; :: thesis:
let x be Point of X; :: thesis:
let y be Point of Y; :: thesis:
assume A4: x = y ; :: thesis:
assume A5: g is_continuous_at y ; :: thesis:
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 )

let G be Subset of Z; :: thesis:
assume ( G is open & f . x in G ) ; :: thesis:
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:
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:

end;