set G1 = G .set (WeightSelector,X);
( dom G c= dom (G .set (WeightSelector,X)) & ELabelSelector in dom G )
by Def5, FUNCT_4:10;
hence
ELabelSelector in dom (G .set (WeightSelector,X))
; GLIB_003:def 5 ex f being Function st
( (G .set (WeightSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (WeightSelector,X)) )
G == G .set (WeightSelector,X)
by Lm3;
then A1:
the_Edges_of G = the_Edges_of (G .set (WeightSelector,X))
;
( (G .set (WeightSelector,X)) . ELabelSelector = the_ELabel_of G & dom (the_ELabel_of G) c= the_Edges_of G )
by Lm1, GLIB_000:9;
hence
ex f being Function st
( (G .set (WeightSelector,X)) . ELabelSelector = f & dom f c= the_Edges_of (G .set (WeightSelector,X)) )
by A1; verum