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 :: thesis: ( ex y9 being finite set ex z being set st
( [x,y] = [y9,z] & y9 in dom f & z in f . y9 ) implies ( x is finite & x in dom f & y in f . x ) )

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, XTUPLE_0:1;
hence ( x is finite & x in dom f & y in f . x ) by A1, A2, XTUPLE_0:1; :: thesis: verum

end;

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