let G2 be loopless _Graph; :: thesis: for V being Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V holds
( the_Edges_of G2 misses G1 .loops() & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops()) )
let V be Subset of (the_Vertices_of G2); :: thesis: for G1 being addLoops of G2,V holds
( the_Edges_of G2 misses G1 .loops() & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops()) )
let G1 be addLoops of G2,V; :: thesis: ( the_Edges_of G2 misses G1 .loops() & the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops()) )
thus the_Edges_of G2 misses G1 .loops() :: thesis: the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops())

proof

assume the_Edges_of G2 meets G1 .loops() ; :: thesis: contradiction
then consider e being object such that
A1: ( e in the_Edges_of G2 & e in G1 .loops() ) by XBOOLE_0:3;
consider v being object such that
A2: e Joins v,v,G1 by A1, GLIB_009:def 2;
thus contradiction by A1, A2, GLIB_006:72, GLIB_000:18; :: thesis: verum

end;

consider E being set , f being one-to-one Function such that
A3: ( 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;

now :: thesis: for e being object holds
( ( e in G1 .loops() implies e in E ) & ( e in E implies e in G1 .loops() ) )

let e be object ; :: thesis: ( ( e in G1 .loops() implies e in E ) & ( e in E implies e in G1 .loops() ) )

hereby :: thesis: ( e in E implies e in G1 .loops() )

assume e in G1 .loops() ; :: thesis: e in E
then consider v being object such that
A4: e Joins v,v,G1 by GLIB_009:def 2;
A5: not e in the_Edges_of G2 by A4, GLIB_000:18, GLIB_006:72;
e in the_Edges_of G1 by A4, GLIB_000:def 13;
hence e in E by A3, A5, XBOOLE_0:def 3; :: thesis: verum

end;

assume e in E ; :: thesis: e in G1 .loops()
then A6: ( e in dom f & e in the_Edges_of G1 ) by A3, XBOOLE_0:def 3;
then ( (the_Source_of G1) . e = f . e & (the_Target_of G1) . e = f . e ) by A3, FUNCT_4:13;
hence e in G1 .loops() by A6, GLIB_000:def 14, GLIB_009:45; :: thesis: verum

end;

hence the_Edges_of G1 = (the_Edges_of G2) \/ (G1 .loops()) by A3, TARSKI:2; :: thesis: verum