:: deftheorem defines weight-preserving GLIB_010:def 25 :
for G1, G2 being WGraph
for F being PGraphMapping of G1,G2 holds
( F is weight-preserving iff (the_Weight_of G2) * (F _E) = (the_Weight_of G1) | (dom (F _E)) );