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; :: according to GLIB_010:def 2 :: thesis: ex f being ManySortedSet of the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) st (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = f

consider f being ManySortedSet of the_Vertices_of G1 such that

A1: G1 . VLabelSelector = f by Def2;

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 the_Vertices_of G1 = the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) by GLIB_007:4;

then reconsider f = f as ManySortedSet of the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) ;

take f ; :: thesis: (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = f

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: verum

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; :: according to GLIB_010:def 2 :: thesis: ex f being ManySortedSet of the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) st (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = f

consider f being ManySortedSet of the_Vertices_of G1 such that

A1: G1 . VLabelSelector = f by Def2;

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 the_Vertices_of G1 = the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) by GLIB_007:4;

then reconsider f = f as ManySortedSet of the_Vertices_of (G2 .set (VLabelSelector,(the_VLabel_of G1))) ;

take f ; :: thesis: (G2 .set (VLabelSelector,(the_VLabel_of G1))) . VLabelSelector = f

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: verum