set G1 = G .set ELabelSelector ,X;
( dom (G .set ELabelSelector ,X) = (dom G) \/ {ELabelSelector } & ELabelSelector in {ELabelSelector } ) by GLIB_000:9, TARSKI:def 1;
hence ELabelSelector in dom (G .set ELabelSelector ,X) by XBOOLE_0:def 3; :: according to GLIB_003:def 5 :: thesis: ex f being Function st
( (G .set ELabelSelector ,X) . ELabelSelector = f & dom f c= the_Edges_of (G .set ELabelSelector ,X) )
G == G .set ELabelSelector ,X by Lm3;
then A1: the_Edges_of G = the_Edges_of (G .set ELabelSelector ,X) by GLIB_000:def 36;
dom X = the_Edges_of G by PARTFUN1:def 4;
hence ex f being Function st
( (G .set ELabelSelector ,X) . ELabelSelector = f & dom f c= the_Edges_of (G .set ELabelSelector ,X) ) by A1, GLIB_000:11; :: thesis: verum