let x, y be set ; :: 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: ( [y,x] `1 = y & [y,x] `2 = x ) by MCART_1:7;
( [x,y] in *graph f iff [y,x] in Union (disjoin f) ) by RELAT_1:def 7;
hence ( [x,y] in *graph f iff ( x in dom f & y in f . x ) ) by A1, CARD_3:33; :: thesis: verum