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 ;
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 ;
hence ( x = (f ") . y1 or x = (f ") . y2 ) by ; :: thesis: verum
end;
thus ( ( x = (f ") . y1 or x = (f ") . y2 ) implies x in dom f ) by ; :: thesis: verum
end;
hence dom f = {((f ") . y1),((f ") . y2)} by TARSKI:def 2; :: thesis: verum