let X, Y be non empty TopSpace; :: thesis: for x being Point of X
for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f " = <:(Y --> x),(id Y):>
let x be Point of X; :: thesis: for f being Function of [:(X | {x}),Y:],Y st f = pr2 ({x}, the carrier of Y) holds
f " = <:(Y --> x),(id Y):>
let f be Function of [:(X | {x}),Y:],Y; :: thesis: ( f = pr2 ({x}, the carrier of Y) implies f " = <:(Y --> x),(id Y):> )
set Z = {x};
set idY = id Y;
A1: rng (id Y) c= the carrier of Y ;
assume A2: f = pr2 ({x}, the carrier of Y) ; :: thesis: f " = <:(Y --> x),(id Y):>
then A3: rng f = the carrier of Y by FUNCT_3:46;
reconsider Z = {x} as non empty Subset of X ;
reconsider idZ = Y --> x as continuous Function of Y,(X | Z) by Th2;
reconsider KA = <:idZ,(id Y):> as continuous Function of Y,[:(X | Z),Y:] by YELLOW12:41;
A4: [:{x}, the carrier of Y:] c= rng KA

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [:{x}, the carrier of Y:] or y in rng KA )
assume y in [:{x}, the carrier of Y:] ; :: thesis: y in rng KA
then consider y1, y2 being object such that
A5: y1 in {x} and
A6: y2 in the carrier of Y and
A7: y = [y1,y2] by ZFMISC_1:def 2;
A8: y = [x,y2] by A5, A7, TARSKI:def 1;
A9: idZ . y2 = ( the carrier of Y --> x) . y2
.= x by A6, FUNCOP_1:7 ;
A10: y2 in dom KA by A6, FUNCT_2:def 1;
then KA . y2 = [(idZ . y2),((id Y) . y2)] by FUNCT_3:def 7
.= [x,y2] by A6, A9, FUNCT_1:18 ;
hence y in rng KA by A8, A10, FUNCT_1:def 3; :: thesis: verum

end;

rng idZ c= the carrier of (X | Z) ;
then A11: rng idZ c= Z by PRE_TOPC:8;
then ( rng KA c= [:(rng idZ),(rng (id Y)):] & [:(rng idZ),(rng (id Y)):] c= [:{x}, the carrier of Y:] ) by FUNCT_3:51, ZFMISC_1:96;
then rng KA c= [:{x}, the carrier of Y:] ;
then A12: rng KA = [:Z, the carrier of Y:] by A4
.= dom f by A2, FUNCT_3:def 5 ;
A13: f is one-to-one by A2, Th5;
A14: f is onto by A3, FUNCT_2:def 3;
dom idZ = the carrier of Y by FUNCT_2:def 1
.= dom (id Y) by FUNCT_2:def 1 ;
then f * KA = id (rng f) by A2, A3, A11, A1, FUNCT_3:52;
then KA = f " by A13, A12, FUNCT_1:42;
hence f " = <:(Y --> x),(id Y):> by A13, A14, TOPS_2:def 4; :: thesis: verum