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