let f be Relation; for x, y being object st dom f = {x} & rng f = {y} holds
f = {[x,y]}
let x, y be object ; ( dom f = {x} & rng f = {y} implies f = {[x,y]} )
A1:
f c= [:(dom f),(rng f):]
by Th1;
assume A2:
( dom f = {x} & rng f = {y} )
; f = {[x,y]}
x in dom f
by A2, TARSKI:def 1;
then consider yy being object such that
A3:
[x,yy] in f
by XTUPLE_0:def 12;
yy in rng f
by A3, XTUPLE_0:def 13;
then
[x,y] in f
by A3, A2, TARSKI:def 1;
hence
f = {[x,y]}
by A1, A2, ZFMISC_1:29, ZFMISC_1:31; verum