let G be WGraph; :: thesis: ( G == G .strict WGraphSelectors & the_Weight_of G = the_Weight_of (G .strict WGraphSelectors ) )
set G2 = G .strict WGraphSelectors ;
A1: ( VertexSelector in WGraphSelectors & EdgeSelector in WGraphSelectors & SourceSelector in WGraphSelectors & TargetSelector in WGraphSelectors & WeightSelector in WGraphSelectors ) by ENUMSET1:def 3;
then A2: the_Vertices_of (G .strict WGraphSelectors ) = the_Vertices_of G by FUNCT_1:72;
A3: the_Edges_of (G .strict WGraphSelectors ) = the_Edges_of G by A1, FUNCT_1:72;
A4: the_Source_of (G .strict WGraphSelectors ) = the_Source_of G by A1, FUNCT_1:72;
the_Target_of (G .strict WGraphSelectors ) = the_Target_of G by A1, FUNCT_1:72;
hence G == G .strict WGraphSelectors by A2, A3, A4, GLIB_000:def 36; :: thesis: the_Weight_of G = the_Weight_of (G .strict WGraphSelectors )
thus the_Weight_of G = the_Weight_of (G .strict WGraphSelectors ) by A1, FUNCT_1:72; :: thesis: verum