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 is one-to-one
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 is one-to-one
let f be Function of [:(X | {x}),Y:],Y; :: thesis: ( f = pr2 {x},the carrier of Y implies f is one-to-one )
set Z = {x};
assume A1: f = pr2 {x},the carrier of Y ; :: thesis: f is one-to-one
then A2: dom f = [:{x},the carrier of Y:] by FUNCT_3:def 6;
let z, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y )
assume that
A3: ( z in dom f & y in dom f ) and
A4: f . z = f . y ; :: thesis: z = y
consider x1, x2 being set such that
A5: ( x1 in {x} & x2 in the carrier of Y & z = [x1,x2] ) by A2, A3, ZFMISC_1:def 2;
consider y1, y2 being set such that
A6: ( y1 in {x} & y2 in the carrier of Y & y = [y1,y2] ) by A2, A3, ZFMISC_1:def 2;
A7: x1 = x by A5, TARSKI:def 1
.= y1 by A6, TARSKI:def 1 ;
x2 = f . x1,x2 by A1, A5, FUNCT_3:def 6
.= f . y1,y2 by A4, A5, A6
.= y2 by A1, A6, FUNCT_3:def 6 ;
hence z = y by A5, A6, A7; :: thesis: verum