let x, y be object ; :: 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 A2: x in dom f by XTUPLE_0:def 12; :: thesis: y = f . x
reconsider y = y as set by TARSKI:1;
y = f . x by A1, Def2, A2;
hence y = f . x ; :: thesis: verum

end;

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