let f be one-to-one Function; :: thesis: for y1, y2 being object st rng f = {y1,y2} holds
dom f = {((f ") . y1),((f ") . y2)}
let y1, y2 be object ; :: thesis: ( rng f = {y1,y2} implies dom f = {((f ") . y1),((f ") . y2)} )
assume A1: rng f = {y1,y2} ; :: thesis: dom f = {((f ") . y1),((f ") . y2)}
then A2: ( y1 in rng f & y2 in rng f ) by TARSKI:def 2;
then consider x1 being object such that
A3: ( x1 in dom f & f . x1 = y1 ) by FUNCT_1:def 3;
consider x2 being object such that
A4: ( x2 in dom f & f . x2 = y2 ) by A2, FUNCT_1:def 3;
for x being object holds
( x in dom f iff ( x = (f ") . y1 or x = (f ") . y2 ) )

proof

let x be object ; :: thesis: ( x in dom f iff ( x = (f ") . y1 or x = (f ") . y2 ) )
thus ( not x in dom f or x = (f ") . y1 or x = (f ") . y2 ) :: thesis: ( ( x = (f ") . y1 or x = (f ") . y2 ) implies x in dom f )

proof

assume A5: x in dom f ; :: thesis: ( x = (f ") . y1 or x = (f ") . y2 )
then f . x in rng f by FUNCT_1:3;
then ( f . x = y1 or f . x = y2 ) by A1, TARSKI:def 2;
hence ( x = (f ") . y1 or x = (f ") . y2 ) by A5, FUNCT_1:34; :: thesis: verum

end;

thus ( ( x = (f ") . y1 or x = (f ") . y2 ) implies x in dom f ) by A3, A4, FUNCT_1:34; :: thesis: verum

end;

hence dom f = {((f ") . y1),((f ") . y2)} by TARSKI:def 2; :: thesis: verum