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 y' being finite set , z being set such that A1: ( [x,y] = [y',z] & y' in dom f & z in f . y' ) ; :: thesis: ( x is finite & x in dom f & y in f . x )
( x = y' & y = z ) by A1, ZFMISC_1:33;
hence ( x is finite & x in dom f & y in f . x ) by A1; :: 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