let f be Relation; :: thesis: for x, y being object st dom f = {x} & rng f = {y} holds
f = {[x,y]}
let x, y be object ; :: thesis: ( 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} ) ; :: thesis: 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; :: thesis: verum