set G1 = G .set WeightSelector ,X;
A1: dom G c= dom (G .set WeightSelector ,X) by FUNCT_4:11;
VLabelSelector in dom G by Def6;
hence VLabelSelector in dom (G .set WeightSelector ,X) by A1; :: according to GLIB_003:def 6 :: thesis: ex f being Function st
( (G .set WeightSelector ,X) . VLabelSelector = f & dom f c= the_Vertices_of (G .set WeightSelector ,X) )
G == G .set WeightSelector ,X by Lm3;
then A2: the_Vertices_of G = the_Vertices_of (G .set WeightSelector ,X) by GLIB_000:def 36;
A3: (G .set WeightSelector ,X) . VLabelSelector = the_VLabel_of G by GLIB_000:12;
dom (the_VLabel_of G) c= the_Vertices_of G by Lm2;
hence ex f being Function st
( (G .set WeightSelector ,X) . VLabelSelector = f & dom f c= the_Vertices_of (G .set WeightSelector ,X) ) by A2, A3; :: thesis: verum