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