set G1 = G .set (ELabelSelector,X);
( dom G c= dom (G .set (ELabelSelector,X)) & VLabelSelector in dom G )
by Def6, FUNCT_4:10;
hence
VLabelSelector in dom (G .set (ELabelSelector,X))
; GLIB_003:def 6 ex f being Function st
( (G .set (ELabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (ELabelSelector,X)) )
G == G .set (ELabelSelector,X)
by Lm3;
then A2:
the_Vertices_of G = the_Vertices_of (G .set (ELabelSelector,X))
;
( (G .set (ELabelSelector,X)) . VLabelSelector = the_VLabel_of G & dom (the_VLabel_of G) c= the_Vertices_of G )
by Lm2, GLIB_000:9;
hence
ex f being Function st
( (G .set (ELabelSelector,X)) . VLabelSelector = f & dom f c= the_Vertices_of (G .set (ELabelSelector,X)) )
by A2; verum