A1: dom (the_Weight_of G) = the_Edges_of G by PARTFUN1:def 2;
then rng (the_Weight_of G) is finite by FINSET_1:8;
hence the_Weight_of G is finite by A1, ORDERS_1:87; :: thesis: verum