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