set G1 = G .set VLabelSelector ,X;
A1: dom (G .set VLabelSelector ,X) = (dom G) \/ {VLabelSelector } by GLIB_000:9;
VLabelSelector in {VLabelSelector } by TARSKI:def 1;
hence VLabelSelector in dom (G .set VLabelSelector ,X) by A1, XBOOLE_0:def 3; :: according to GLIB_003:def 6 :: thesis: ex f being Function st
( (G .set VLabelSelector ,X) . VLabelSelector = f & dom f c= the_Vertices_of (G .set VLabelSelector ,X) )
G == G .set VLabelSelector ,X by Lm3;
then A2: the_Vertices_of G = the_Vertices_of (G .set VLabelSelector ,X) by GLIB_000:def 36;
dom X = the_Vertices_of G by PARTFUN1:def 4;
hence ex f being Function st
( (G .set VLabelSelector ,X) . VLabelSelector = f & dom f c= the_Vertices_of (G .set VLabelSelector ,X) ) by A2, GLIB_000:11; :: thesis: verum