let X, Y be non empty TopSpace; :: thesis: for x being Point of X holds Y --> x is continuous Function of Y,(X | {x})
let x be Point of X; :: thesis: Y --> x is continuous Function of Y,(X | {x})
set Z = {x};
set f = Y --> x;
( x in {x} & the carrier of (X | {x}) = {x} ) by PRE_TOPC:8, TARSKI:def 1;
then reconsider g = Y --> x as Function of Y,(X | {x}) by FUNCOP_1:45;
g is continuous by TOPMETR:6;
hence Y --> x is continuous Function of Y,(X | {x}) ; :: thesis: verum