let f be Function; :: thesis: for x, y being set holds
( [x,y] in graph f iff ( x is finite & x in dom f & y in f . x ) )
let x, y be set ; :: thesis: ( [x,y] in graph f iff ( x is finite & x in dom f & y in f . x ) )

now

given y9 being finite set , z being set such that A1: [x,y] = [y9,z] and
A2: ( y9 in dom f & z in f . y9 ) ; :: thesis: ( x is finite & x in dom f & y in f . x )
x = y9 by A1, ZFMISC_1:27;
hence ( x is finite & x in dom f & y in f . x ) by A1, A2, ZFMISC_1:27; :: thesis: verum

end;

hence ( [x,y] in graph f iff ( x is finite & x in dom f & y in f . x ) ) by Def17; :: thesis: verum