let G1 be addLoops of G,V; :: thesis: G1 is locally-finite

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

suppose A1: V c= the_Vertices_of G ; :: thesis: G1 is locally-finite

let v1 be Vertex of G1; :: according to GLIB_013:def 5 :: thesis: v1 .edgesInOut() is finite
reconsider v2 = v1 as Vertex of G by A1, GLIB_012:def 5;

per cases ( v1 in V or not v1 in V ) ;

suppose v1 in V ; :: thesis: v1 .edgesInOut() is finite

then consider e being object such that
( e DJoins v1,v1,G1 & not e in the_Edges_of G ) and
v1 .edgesIn() = (v2 .edgesIn()) \/ {e} and
v1 .edgesOut() = (v2 .edgesOut()) \/ {e} and
A2: v1 .edgesInOut() = (v2 .edgesInOut()) \/ {e} by A1, GLIB_012:42;
thus v1 .edgesInOut() is finite by A2; :: thesis: verum

end;

suppose not v1 in V ; :: thesis: v1 .edgesInOut() is finite

then v1 .edgesInOut() = v2 .edgesInOut() by A1, GLIB_012:44;
hence v1 .edgesInOut() is finite ; :: thesis: verum

end;

end;

end;

suppose not V c= the_Vertices_of G ; :: thesis: G1 is locally-finite

then G1 == G by GLIB_012:def 5;
hence G1 is locally-finite by Th24; :: thesis: verum

end;

end;