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