defpred S₁[ object , object ] means ex G being _Graph st
( G = F . $1 & $2 = the_Vertices_of G );
A1: for x, y1, y2 being object st x in dom F & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: for x being object st x in dom F holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in dom F implies ex y being object st S₁[x,y] )
assume x in dom F ; :: thesis: ex y being object st S₁[x,y]
then reconsider G = F . x as _Graph by GLIB_000:def 53;
take the_Vertices_of G ; :: thesis: S₁[x, the_Vertices_of G]
take G ; :: thesis: ( G = F . x & the_Vertices_of G = the_Vertices_of G )
thus ( G = F . x & the_Vertices_of G = the_Vertices_of G ) ; :: thesis: verum

end;

consider f being Function such that
A3: ( dom f = dom F & ( for x being object st x in dom F holds
S₁[x,f . x] ) ) from FUNCT_1:sch 2(A1, A2);
take f ; :: thesis: ( dom f = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f . x = the_Vertices_of G ) ) )
thus ( dom f = dom F & ( for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f . x = the_Vertices_of G ) ) ) by A3; :: thesis: verum