set G1 = G .set (WeightSelector,X);
( dom (G .set (WeightSelector,X)) = (dom G) \/ {WeightSelector} & WeightSelector in {WeightSelector} ) by GLIB_000:7, TARSKI:def 1;
hence WeightSelector in dom (G .set (WeightSelector,X)) by XBOOLE_0:def 3; :: according to GLIB_003:def 4 :: thesis: (G .set (WeightSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (WeightSelector,X))
G == G .set (WeightSelector,X) by Lm3;
then the_Edges_of G = the_Edges_of (G .set (WeightSelector,X)) ;
hence (G .set (WeightSelector,X)) . WeightSelector is ManySortedSet of the_Edges_of (G .set (WeightSelector,X)) by GLIB_000:8; :: thesis: verum