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