let X, Y be non empty TopSpace; :: thesis:
let x be Point of X; :: thesis:
let f be Function of [:(X | {x}),Y:],Y; :: thesis:
set Z = {x};
assume A1: f = pr2 {x},the carrier of Y ; :: thesis:
then A2: rng f = the carrier of Y by FUNCT_3:62;
A3: f is one-to-one by A1, Th7;
reconsider Z = {x} as non empty Subset of X ;
reconsider idZ = Y --> x as continuous Function of Y,(X | Z) by Th2;
set idY = id Y;
reconsider KA = <:idZ,(id Y):> as continuous Function of Y,[:(X | Z),Y:] by YELLOW12:41;
A4: rng KA c= [:(rng idZ),(rng (id Y)):] by FUNCT_3:71;
rng idZ c= the carrier of (X | Z) ;
then A5: rng idZ c= Z by PRE_TOPC:29;
then [:(rng idZ),(rng (id Y)):] c= [:{x},the carrier of Y:] by ZFMISC_1:119;
then A6: rng KA c= [:{x},the carrier of Y:] by A4, XBOOLE_1:1;
[:{x},the carrier of Y:] c= rng KA

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in [:{x},the carrier of Y:] ; :: thesis:
then consider y1, y2 being set such that
A7: ( y1 in {x} & y2 in the carrier of Y & y = [y1,y2] ) by ZFMISC_1:def 2;
A8: y = [x,y2] by A7, TARSKI:def 1;
A9: idZ . y2 = (the carrier of Y --> x) . y2
.= x by A7, FUNCOP_1:13 ;
A10: y2 in dom KA by A7, FUNCT_2:def 1;
then KA . y2 = [(idZ . y2),((id Y) . y2)] by FUNCT_3:def 8
.= [x,y2] by A7, A9, FUNCT_1:35 ;
hence y in rng KA by A8, A10, FUNCT_1:def 5; :: thesis:

end;

then A11: rng KA = [:Z,the carrier of Y:] by A6, XBOOLE_0:def 10
.= dom f by A1, FUNCT_3:def 6 ;
A12: dom idZ = the carrier of Y by FUNCT_2:def 1
.= dom (id Y) by FUNCT_2:def 1 ;
rng (id Y) c= the carrier of Y ;
then f * KA = id (rng f) by A1, A2, A5, A12, FUNCT_3:72;
then KA = f " by A3, A11, FUNCT_1:64;
hence f " = <:(Y --> x),(id Y):> by A1, A2, Th7, TOPS_2:def 4; :: thesis: