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
let z, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not z in dom f or not y in dom f or not f . z = f . y or z = y )
assume that
A2: z in dom f and
A3: y in dom f and
A4: f . z = f . y ; :: thesis: z = y
A5: dom f = [:{x}, the carrier of Y:] by A1, FUNCT_3:def 5;
then consider x1, x2 being object such that
A6: x1 in {x} and
A7: x2 in the carrier of Y and
A8: z = [x1,x2] by A2, ZFMISC_1:def 2;
consider y1, y2 being object such that
A9: y1 in {x} and
A10: y2 in the carrier of Y and
A11: y = [y1,y2] by A5, A3, ZFMISC_1:def 2;
A12: x1 = x by A6, TARSKI:def 1
.= y1 by A9, TARSKI:def 1 ;
x2 = f . (x1,x2) by A1, A6, A7, FUNCT_3:def 5
.= f . (y1,y2) by A4, A8, A11
.= y2 by A1, A9, A10, FUNCT_3:def 5 ;
hence z = y by A8, A11, A12; :: thesis: verum