let f be Function; :: thesis: f = { [x,(f . x)] where x is Element of dom f : x in dom f }
set RH = { [x,(f . x)] where x is Element of dom f : x in dom f } ;

now

let z be set ; :: thesis: ( z in f implies z in { [x,(f . x)] where x is Element of dom f : x in dom f } )
assume C2: z in f ; :: thesis: z in { [x,(f . x)] where x is Element of dom f : x in dom f }
then consider x, y being set such that
C0: z = [x,y] by RELAT_1:def 1;
reconsider xx = x as Element of dom f by C0, C2, FUNCT_1:1;
( z = [xx,(f . xx)] & xx in dom f ) by C0, C2, FUNCT_1:1;
hence z in { [x,(f . x)] where x is Element of dom f : x in dom f } ; :: thesis: verum

end;

then B0: f c= { [x,(f . x)] where x is Element of dom f : x in dom f } by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in { [x,(f . x)] where x is Element of dom f : x in dom f } implies z in f )
assume C0: z in { [x,(f . x)] where x is Element of dom f : x in dom f } ; :: thesis: z in f
consider x being Element of dom f such that
D0: ( z = [x,(f . x)] & x in dom f ) by C0;
thus z in f by D0, FUNCT_1:1; :: thesis: verum

end;

then { [x,(f . x)] where x is Element of dom f : x in dom f } c= f by TARSKI:def 3;
hence f = { [x,(f . x)] where x is Element of dom f : x in dom f } by B0, XBOOLE_0:def 10; :: thesis: verum