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

proof

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

end;

rng idY c= the carrier of (X | Z) ;
then A10: rng idY c= Z by PRE_TOPC:8;
then ( rng KA c= [:(rng (id Y)),(rng idY):] & [:(rng (id Y)),(rng idY):] c= [: the carrier of Y,Z:] ) by FUNCT_3:51, ZFMISC_1:96;
then rng KA c= [: the carrier of Y,Z:] ;
then A11: rng KA = [: the carrier of Y,Z:] by A4
.= dom f by A2, FUNCT_3:def 4 ;
A12: f is one-to-one by A2, Th4;
A13: f is onto by A3, FUNCT_2:def 3;
dom idY = 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, A10, A1, FUNCT_3:52;
then KA = f " by A12, A11, FUNCT_1:42;
hence f " = <:(id Y),(Y --> x):> by A12, A13, TOPS_2:def 4; :: thesis: verum