set G3 = G2 .set (ELabelSelector,(the_ELabel_of G1));
ELabelSelector in {ELabelSelector} by TARSKI:def 1;
then ELabelSelector in (dom G2) \/ {ELabelSelector} by XBOOLE_0:def 3;
hence ELabelSelector in dom (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_000:7; :: according to GLIB_010:def 1 :: thesis: ex f being ManySortedSet of the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) st (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f
consider f being ManySortedSet of the_Edges_of G1 such that
A1: G1 . ELabelSelector = f by Def1;
G2 == G2 .set (ELabelSelector,(the_ELabel_of G1)) by GLIB_003:7;
then the_Edges_of G2 = the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_000:def 34;
then the_Edges_of G1 = the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) by GLIB_007:4;
then reconsider f = f as ManySortedSet of the_Edges_of (G2 .set (ELabelSelector,(the_ELabel_of G1))) ;
take f ; :: thesis: (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = f
thus (G2 .set (ELabelSelector,(the_ELabel_of G1))) . ELabelSelector = the_ELabel_of G1 by GLIB_000:8
.= f by A1, GLIB_003:def 8 ; :: thesis: verum