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; GLIB_010:def 2 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
; (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
; verum