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

( [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