ex f being Function st
( G . VLabelSelector = f & dom f c= the_Vertices_of G ) by Def6;
hence G . VLabelSelector is Function ; :: thesis: verum