let f be one-to-one Function; :: thesis: for y being object st rng f = {y} holds
dom f = {((f ") . y)}
let y be object ; :: thesis: ( rng f = {y} implies dom f = {((f ") . y)} )
assume A1: rng f = {y} ; :: thesis: dom f = {((f ") . y)}
then y in rng f by TARSKI:def 1;
then consider x0 being object such that
A2: ( x0 in dom f & f . x0 = y ) by FUNCT_1:def 3;
for x being object holds
( x in dom f iff x = (f ") . y )

proof

let x be object ; :: thesis: ( x in dom f iff x = (f ") . y )

hereby :: thesis: ( x = (f ") . y implies x in dom f )

assume A3: x in dom f ; :: thesis: x = (f ") . y
then f . x in rng f by FUNCT_1:3;
then f . x = y by A1, TARSKI:def 1;
hence x = (f ") . y by A3, FUNCT_1:34; :: thesis: verum

end;

assume x = (f ") . y ; :: thesis: x in dom f
hence x in dom f by A2, FUNCT_1:34; :: thesis: verum

end;

hence dom f = {((f ") . y)} by TARSKI:def 1; :: thesis: verum