let x, y be object ; :: thesis: for f being Function holds
( [x,y] in *graph f iff ( x in dom f & y in f . x ) )
let f be Function; :: thesis: ( [x,y] in *graph f iff ( x in dom f & y in f . x ) )
A1: ( [x,y] in *graph f iff [y,x] in Union (disjoin f) ) by RELAT_1:def 7;
( [y,x] `1 = y & [y,x] `2 = x ) ;
hence ( [x,y] in *graph f iff ( x in dom f & y in f . x ) ) by A1, CARD_3:22; :: thesis: verum