let x1, x2 be set ; :: thesis: ( x1 in dom f & f . x1 = y & x2 in dom f & f . x2 = y implies x1 = x2 )
assume that
A3: ( x1 in dom f & f . x1 = y ) and
A4: ( x2 in dom f & f . x2 = y ) ; :: thesis: x1 = x2
consider x being set such that
x in dom f and
f . x = y and
A5: for z being set st z in dom f & z <> x holds
f . z <> y by A1, Th9;
x = x1 by A3, A5;
hence x1 = x2 by A4, A5; :: thesis: verum