set G3 = G2 .set (VLabelSelector,(the_VLabel_of G1));
VLabelSelector in {VLabelSelector} by TARSKI:def 1;
then VLabelSelector in (dom G2) \/ {VLabelSelector} by XBOOLE_0:def 3;
hence VLabelSelector in dom (G2 .set (VLabelSelector,(the_VLabel_of G1))) by GLIB_000:7; :: thesis: ex f being Function st
( (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = f & dom f c= the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) )
consider f being Function such that
A1: ( G1 . VLabelSelector = f & dom f c= the_Vertices_of G1 ) by GLIB_003:def 6;
G2 == G2 .set (VLabelSelector,(the_VLabel_of G1)) by GLIB_003:7;
then the_Vertices_of G2 = the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) by GLIB_000:def 34;
then A2: the_Vertices_of G1 = the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) by GLIB_007:4;
take f = f; :: thesis: ( (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = f & dom f c= the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) )
thus (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = the_VLabel_of G1 by GLIB_000:8
.= f by A1, GLIB_003:def 9 ; :: thesis: dom f c= the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1)))
thus dom f c= the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) by A1, A2; :: thesis: verum