set G1 = G .set WeightSelector ,X;
A1: dom (G .set WeightSelector ,X) = (dom G) \/ {WeightSelector } by GLIB_000:9;
WeightSelector in {WeightSelector } by TARSKI:def 1;
hence WeightSelector in dom (G .set WeightSelector ,X) by A1, 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) by GLIB_000:def 36;
hence (G .set WeightSelector ,X) . WeightSelector is ManySortedSet of the_Edges_of (G .set WeightSelector ,X) by GLIB_000:11; :: thesis: verum