now :: thesis: for x being object st x in dom (the_Vertices_of F) holds
not (the_Vertices_of F) . x is empty

let x be object ; :: thesis: ( x in dom (the_Vertices_of F) implies not (the_Vertices_of F) . x is empty )
assume x in dom (the_Vertices_of F) ; :: thesis: not (the_Vertices_of F) . x is empty
then x in dom F by Def4;
then consider G being _Graph such that
A1: ( G = F . x & (the_Vertices_of F) . x = the_Vertices_of G ) by Def4;
thus not (the_Vertices_of F) . x is empty by A1; :: thesis: verum

end;

hence the_Vertices_of F is non-empty by FUNCT_1:def 9; :: thesis: verum