let G1 be addLoops of G,V; :: thesis: G1 is edge-finite
consider E being set , f being one-to-one Function such that
A1: ( E misses the_Edges_of G & the_Edges_of G1 = (the_Edges_of G) \/ E ) and
A2: ( dom f = E & rng f = V ) and
( the_Source_of G1 = (the_Source_of G) +* f & the_Target_of G1 = (the_Target_of G) +* f ) by GLIB_012:def 5;
card E = card V by A2, CARD_1:70;
then E is finite ;
hence G1 is edge-finite by A1; :: thesis: verum