let x, y be set ; :: thesis: for f being Function holds
( [x,y] in f iff ( x in dom f & y = f . x ) )
let f be Function; :: thesis: ( [x,y] in f iff ( x in dom f & y = f . x ) )
thus ( [x,y] in f implies ( x in dom f & y = f . x ) ) :: thesis: ( x in dom f & y = f . x implies [x,y] in f )

proof

assume A1: [x,y] in f ; :: thesis: ( x in dom f & y = f . x )
hence x in dom f by RELAT_1:def 4; :: thesis: y = f . x
hence y = f . x by A1, Def4; :: thesis: verum

end;

thus ( x in dom f & y = f . x implies [x,y] in f ) by Def4; :: thesis: verum