let G be _Graph; :: thesis: ( not G is vertex-finite & G is loopfull implies not G is edge-finite )
assume A3: ( not G is vertex-finite & G is loopfull ) ; :: thesis: not G is edge-finite
G .loops() is infinite

proof

assume A4: G .loops() is finite ; :: thesis: contradiction
set f = (the_Source_of G) | (G .loops());

now :: thesis: for v being object st v in the_Vertices_of G holds
v in rng ((the_Source_of G) | (G .loops()))

let v be object ; :: thesis: ( v in the_Vertices_of G implies v in rng ((the_Source_of G) | (G .loops())) )
assume v in the_Vertices_of G ; :: thesis: v in rng ((the_Source_of G) | (G .loops()))
then consider e being object such that
A5: e Joins v,v,G by A3, GLIB_012:def 1;
A6: e in G .loops() by A5, GLIB_009:def 2;
A7: v = (the_Source_of G) . e by A5, GLIB_000:def 13
.= ((the_Source_of G) | (G .loops())) . e by A6, FUNCT_1:49 ;
e in the_Edges_of G by A5, GLIB_000:def 13;
then e in dom (the_Source_of G) by FUNCT_2:def 1;
then e in dom ((the_Source_of G) | (G .loops())) by A6, RELAT_1:57;
hence v in rng ((the_Source_of G) | (G .loops())) by A7, FUNCT_1:def 3; :: thesis: verum

end;

then the_Vertices_of G c= rng ((the_Source_of G) | (G .loops())) by TARSKI:def 3;
hence contradiction by A3, A4; :: thesis: verum

end;

hence not G is edge-finite ; :: thesis: verum