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 :: thesis: for z being object st z in f holds
z in { [x,(f . x)] where x is Element of dom f : x in dom f }
let z be object ; :: thesis: ( z in f implies z in { [x,(f . x)] where x is Element of dom f : x in dom f } )
assume A1: 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 object such that
A2: z = [x,y] by RELAT_1:def 1;
reconsider xx = x as Element of dom f by FUNCT_1:1, A2, A1;
( z = [xx,(f . xx)] & xx in dom f ) by A2, FUNCT_1:1, A1;
hence z in { [x,(f . x)] where x is Element of dom f : x in dom f } ; :: thesis: verum
end;
then A3: f c= { [x,(f . x)] where x is Element of dom f : x in dom f } ;
now :: thesis: for z being object st z in { [x,(f . x)] where x is Element of dom f : x in dom f } holds
z in f
let z be object ; :: thesis: ( z in { [x,(f . x)] where x is Element of dom f : x in dom f } implies z in f )
assume A4: 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
A5: ( z = [x,(f . x)] & x in dom f ) by A4;
thus z in f by A5, FUNCT_1:1; :: thesis: verum
end;
then { [x,(f . x)] where x is Element of dom f : x in dom f } c= f ;
hence f = { [x,(f . x)] where x is Element of dom f : x in dom f } by A3; :: thesis: verum