let f be Function; :: thesis: for x, y being set st f = [x,y] holds
x = y
let x, y be set ; :: thesis: ( f = [x,y] implies x = y )
assume f = [x,y] ; :: thesis: x = y
then A6: ( {x} in f & {x,y} in f ) by TARSKI:def 2;
then consider a, b being set such that
A2: {x} = [a,b] by RELAT_1:def 1;
A5: ( {a} = {a,b} & x = {a} ) by A2, ZFMISC_1:8, ZFMISC_1:9;
consider c, d being set such that
A4: {x,y} = [c,d] by A6, RELAT_1:def 1;
A7: ( ( x = {c} & y = {c,d} ) or ( x = {c,d} & y = {c} ) ) by A4, ZFMISC_1:10;
then c = a by A5, ZFMISC_1:8;
hence x = y by A7, A5, A6, A2, A4, FUNCT_1:def 1; :: thesis: verum