consider f being Function such that
A1: ( G . VLabelSelector = f & dom f c= the_Vertices_of G ) by Def6;
thus G . VLabelSelector is Function by A1; :: thesis: verum