let G2 be _Graph; :: thesis: for V being set
for G1 being addLoops of G2,V holds
( G1 is _finite iff G2 is _finite )
let V be set ; :: thesis: for G1 being addLoops of G2,V holds
( G1 is _finite iff G2 is _finite )
let G1 be addLoops of G2,V; :: thesis: ( G1 is _finite iff G2 is _finite )

per cases ( V c= the_Vertices_of G2 or not V c= the_Vertices_of G2 ) ;

suppose A1: V c= the_Vertices_of G2 ; :: thesis: ( G1 is _finite iff G2 is _finite )

then consider E being set , f being one-to-one Function such that
A2: ( E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E & dom f = E & rng f = V & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f ) by Def5;
thus ( G1 is _finite implies G2 is _finite ) ; :: thesis: ( G2 is _finite implies G1 is _finite )
assume A3: G2 is _finite ; :: thesis: G1 is _finite
then E is finite by A1, A2, CARD_1:59;
then A4: the_Edges_of G1 is finite by A2, A3;
the_Vertices_of G2 = the_Vertices_of G1 by Th15;
hence G1 is _finite by A3, A4, GLIB_000:def 17; :: thesis: verum

end;

suppose not V c= the_Vertices_of G2 ; :: thesis: ( G1 is _finite iff G2 is _finite )

then G1 == G2 by Def5;
hence ( G1 is _finite iff G2 is _finite ) by GLIB_000:89; :: thesis: verum

end;

end;