let f be Function; for x, y being object st f = [x,y] holds
x = y
let x, y be object ; ( f = [x,y] implies x = y )
assume A1:
f = [x,y]
; 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; verum