let G2 be addLoops of G,V; :: thesis: G2 is non-Dmulti

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: G2 is non-Dmulti

now :: thesis: for e1, e2, v1, v2 being object st e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 implies b₁ = b₂ )
assume A2: ( e1 DJoins v1,v2,G2 & e2 DJoins v1,v2,G2 ) ; :: thesis: b₁ = b₂

per cases ( v1 = v2 or v1 <> v2 ) ;

suppose A3: v1 = v2 ; :: thesis: b₁ = b₂

consider E being set , f being one-to-one Function such that
E misses the_Edges_of G and
A4: the_Edges_of G2 = (the_Edges_of G) \/ E and
A5: ( dom f = E & rng f = V ) and
A6: the_Source_of G2 = (the_Source_of G) +* f and
the_Target_of G2 = (the_Target_of G) +* f by A1, Def5;
A7: not e1 in the_Edges_of G

proof

assume A8: e1 in the_Edges_of G ; :: thesis: contradiction
then e1 DJoins v1,v1,G by A2, A3, GLIB_006:71;
then ( (the_Source_of G) . e1 = v1 & (the_Target_of G) . e1 = v1 ) by GLIB_000:def 14;
hence contradiction by A8, GLIB_000:def 18; :: thesis: verum

end;

A9: not e2 in the_Edges_of G

proof

assume A10: e2 in the_Edges_of G ; :: thesis: contradiction
then e2 DJoins v1,v1,G by A2, A3, GLIB_006:71;
then ( (the_Source_of G) . e2 = v1 & (the_Target_of G) . e2 = v1 ) by GLIB_000:def 14;
hence contradiction by A10, GLIB_000:def 18; :: thesis: verum

end;

e1 in the_Edges_of G2 by A2, GLIB_000:def 14;
then A11: e1 in E by A4, A7, XBOOLE_0:def 3;
e2 in the_Edges_of G2 by A2, GLIB_000:def 14;
then A12: e2 in E by A4, A9, XBOOLE_0:def 3;
f . e1 = (the_Source_of G2) . e1 by A5, A6, A11, FUNCT_4:13
.= v1 by A2, GLIB_000:def 14
.= (the_Source_of G2) . e2 by A2, GLIB_000:def 14
.= f . e2 by A5, A6, A12, FUNCT_4:13 ;
hence e1 = e2 by A5, A11, A12, FUNCT_1:def 4; :: thesis: verum

end;

suppose v1 <> v2 ; :: thesis: b₁ = b₂

then ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) by A2, Th16;
hence e1 = e2 by GLIB_000:def 21; :: thesis: verum

end;

end;

end;

hence G2 is non-Dmulti by GLIB_000:def 21; :: thesis: verum

end;

suppose not V c= the_Vertices_of G ; :: thesis: G2 is non-Dmulti

then G == G2 by Def5;
hence G2 is non-Dmulti by GLIB_000:89; :: thesis: verum

end;

end;