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;
A1: Y --> x = the carrier of Y --> x ;
A2: x in {x} by TARSKI:def 1;
the carrier of (X | {x}) = {x} by PRE_TOPC:29;
then reconsider g = Y --> x as Function of Y,(X | {x}) by A1, A2, FUNCOP_1:57;
g is continuous by TOPMETR:9;
hence Y --> x is continuous Function of Y,(X | {x}) ; :: thesis: verum