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