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

proof

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

end;

then A11: rng KA = [:the carrier of Y,Z:] by A6, XBOOLE_0:def 10
.= dom f by A1, FUNCT_3:def 5 ;
A12: dom idY = 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 " = <:(id Y),(Y --> x):> by A1, A2, Th6, TOPS_2:def 4; :: thesis: