let x1, y1, x2, y2 be set ; :: thesis: ( {[x1,y1],[x2,y2]} is Function iff ( x1 = x2 implies y1 = y2 ) )
thus ( {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2 ) :: thesis: ( ( x1 = x2 implies y1 = y2 ) implies {[x1,y1],[x2,y2]} is Function )

proof

A1: ( [x1,y1] in {[x1,y1],[x2,y2]} & [x2,y2] in {[x1,y1],[x2,y2]} ) by TARSKI:def 2;
assume {[x1,y1],[x2,y2]} is Function ; :: thesis: ( not x1 = x2 or y1 = y2 )
hence ( not x1 = x2 or y1 = y2 ) by A1, FUNCT_1:def 1; :: thesis: verum

end;

assume A2: ( x1 = x2 implies y1 = y2 ) ; :: thesis: {[x1,y1],[x2,y2]} is Function

now

thus for p being set st p in {[x1,y1],[x2,y2]} holds
ex x, y being set st [x,y] = p :: thesis: for x, z1, z2 being set st [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} holds
z1 = z2

proof

let p be set ; :: thesis: ( p in {[x1,y1],[x2,y2]} implies ex x, y being set st [x,y] = p )
assume p in {[x1,y1],[x2,y2]} ; :: thesis: ex x, y being set st [x,y] = p
then ( p = [x1,y1] or p = [x2,y2] ) by TARSKI:def 2;
hence ex x, y being set st [x,y] = p ; :: thesis: verum

end;

let x, z1, z2 be set ; :: thesis: ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} implies z1 = z2 )
A3: ( ( not ( [x,z1] = [x1,y1] & [x,z2] = [x1,y1] ) & not ( [x,z1] = [x2,y2] & [x,z2] = [x2,y2] ) ) or ( z1 = y1 & z2 = y1 ) or ( z1 = y2 & z2 = y2 ) ) by ZFMISC_1:33;

A4: now

assume A5: ( ( [x,z1] = [x1,y1] & [x,z2] = [x2,y2] ) or ( [x,z1] = [x2,y2] & [x,z2] = [x1,y1] ) ) ; :: thesis: z1 = z2
then ( x = x1 & x = x2 ) by ZFMISC_1:33;
hence z1 = z2 by A2, A5, ZFMISC_1:33; :: thesis: verum

end;

assume ( [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]} ) ; :: thesis: z1 = z2
hence z1 = z2 by A3, A4, TARSKI:def 2; :: thesis: verum

end;

hence {[x1,y1],[x2,y2]} is Function by FUNCT_1:def 1; :: thesis: verum