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 ) )

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

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

end;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

thus
( ( x = (f ") . y1 or x = (f ") . y2 ) implies x in dom f )
by A3, A4, FUNCT_1:34; :: thesis: verum
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;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