set G2 = G .strict WGraphSelectors ;
A1: dom (G .strict WGraphSelectors ) = (dom G) /\ WGraphSelectors by RELAT_1:90
.= WGraphSelectors by Lm1, XBOOLE_1:28 ;
A2: ( VertexSelector in WGraphSelectors & EdgeSelector in WGraphSelectors & SourceSelector in WGraphSelectors & TargetSelector in WGraphSelectors & WeightSelector in WGraphSelectors ) by ENUMSET1:def 3;
then A3: the_Vertices_of (G .strict WGraphSelectors ) = the_Vertices_of G by FUNCT_1:72;
A4: the_Edges_of (G .strict WGraphSelectors ) = the_Edges_of G by A2, FUNCT_1:72;
A5: the_Source_of (G .strict WGraphSelectors ) = the_Source_of G by A2, FUNCT_1:72;
A6: the_Target_of (G .strict WGraphSelectors ) = the_Target_of G by A2, FUNCT_1:72;
for x being set st x in _GraphSelectors holds
x in dom (G .strict WGraphSelectors ) by A1, A2, ENUMSET1:def 2;
then _GraphSelectors c= dom (G .strict WGraphSelectors ) by TARSKI:def 3;
hence G .strict WGraphSelectors is [Graph-like] by A3, A4, A5, A6, GLIB_000:7; :: thesis: G .strict WGraphSelectors is [Weighted]
(G .strict WGraphSelectors ) . WeightSelector = G . WeightSelector by A2, FUNCT_1:72;
then (G .strict WGraphSelectors ) . WeightSelector is ManySortedSet of by A4, GLIB_003:def 4;
hence G .strict WGraphSelectors is [Weighted] by A1, A2, GLIB_003:def 4; :: thesis: verum