set G1 = G .set (VLabelSelector,X);
( dom G c= dom (G .set (VLabelSelector,X)) & WeightSelector in dom G ) by Def4, FUNCT_4:10;
hence WeightSelector in dom (G .set (VLabelSelector,X)) ; :: according to GLIB_003:def 4 :: thesis: (G .set (VLabelSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (VLabelSelector,X))
G == G .set (VLabelSelector,X) by Lm3;
then A2: the_Edges_of (G .set (VLabelSelector,X)) = the_Edges_of G ;
(G .set (VLabelSelector,X)) . WeightSelector = the_Weight_of G by GLIB_000:9;
hence (G .set (VLabelSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) by A2; :: thesis: verum