let f be Function; :: thesis: ( f = the_Vertices_of F iff ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Vertices_of (F . x) ) ) )

hereby :: thesis: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Vertices_of (F . x) ) implies f = the_Vertices_of F )

assume A1: f = the_Vertices_of F ; :: thesis: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Vertices_of (F . x) ) )
hence dom f = dom F by Def4; :: thesis: for x being Element of dom F holds f . x = the_Vertices_of (F . x)
let x be Element of dom F; :: thesis: f . x = the_Vertices_of (F . x)
consider G being _Graph such that
A2: ( G = F . x & f . x = the_Vertices_of G ) by A1, Def4;
thus f . x = the_Vertices_of (F . x) by A2; :: thesis: verum

end;

assume A3: ( dom f = dom F & ( for x being Element of dom F holds f . x = the_Vertices_of (F . x) ) ) ; :: thesis: f = the_Vertices_of F

now :: thesis: for x being object st x in dom F holds
ex G being _Graph st
( G = F . x & f . x = the_Vertices_of G )

let x be object ; :: thesis: ( x in dom F implies ex G being _Graph st
( G = F . x & f . x = the_Vertices_of G ) )
assume x in dom F ; :: thesis: ex G being _Graph st
( G = F . x & f . x = the_Vertices_of G )
then reconsider x0 = x as Element of dom F ;
reconsider G = F . x0 as _Graph ;
take G = G; :: thesis: ( G = F . x & f . x = the_Vertices_of G )
thus ( G = F . x & f . x = the_Vertices_of G ) by A3; :: thesis: verum

end;

hence f = the_Vertices_of F by A3, Def4; :: thesis: verum