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 )

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

hence
dom f = {((f ") . y)}
by TARSKI:def 1; :: thesis: verum
let x be object ; :: thesis: ( x in dom f iff x = (f ") . y )

hence x in dom f by A2, FUNCT_1:34; :: thesis: verum

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

assume
x = (f ") . y
; :: thesis: x in dom fassume 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;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

hence x in dom f by A2, FUNCT_1:34; :: thesis: verum