let G1 be WGraph; :: thesis: for G2 being WSubgraph of G1
for x being set st x in the_Edges_of G2 holds
(the_Weight_of G2) . x = (the_Weight_of G1) . x
let G2 be WSubgraph of G1; :: thesis: for x being set st x in the_Edges_of G2 holds
(the_Weight_of G2) . x = (the_Weight_of G1) . x
let x be set ; :: thesis: ( x in the_Edges_of G2 implies (the_Weight_of G2) . x = (the_Weight_of G1) . x )
assume x in the_Edges_of G2 ; :: thesis: (the_Weight_of G2) . x = (the_Weight_of G1) . x
then A1: x in dom (the_Weight_of G2) by PARTFUN1:def 2;
the_Weight_of G2 = (the_Weight_of G1) | (the_Edges_of G2) by Def10;
hence (the_Weight_of G2) . x = (the_Weight_of G1) . x by A1, FUNCT_1:47; :: thesis: verum