set G1 = G .set ELabelSelector ,X;
( dom G c= dom (G .set ELabelSelector ,X) & WeightSelector in dom G ) by Def4, FUNCT_4:11;
hence WeightSelector in dom (G .set ELabelSelector ,X) ; :: according to GLIB_003:def 4 :: thesis: (G .set ELabelSelector ,X) . WeightSelector is ManySortedSet of the_Edges_of (G .set ELabelSelector ,X)
G == G .set ELabelSelector ,X by Lm3;
then A1: the_Edges_of (G .set ELabelSelector ,X) = the_Edges_of G by GLIB_000:def 36;
(G .set ELabelSelector ,X) . WeightSelector = the_Weight_of G by GLIB_000:12;
hence (G .set ELabelSelector ,X) . WeightSelector is ManySortedSet of the_Edges_of (G .set ELabelSelector ,X) by A1; :: thesis: verum