let G1, G2 be _Graph; :: thesis: for v being Vertex of G2 holds
( G1 is addLoops of G2,{v} iff ex e being object st
( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v ) )
let v be Vertex of G2; :: thesis: ( G1 is addLoops of G2,{v} iff ex e being object st
( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v ) )

hereby :: thesis: ( ex e being object st
( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v ) implies G1 is addLoops of G2,{v} )

assume A1: G1 is addLoops of G2,{v} ; :: thesis: ex e being object st
( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v )
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;
v in rng f by A2, TARSKI:def 1;
then consider e being object such that
A3: ( e in dom f & f . e = v ) by FUNCT_1:def 3;
take e = e; :: thesis: ( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v )
card E = card {v} by A2, CARD_1:70;
then consider e0 being object such that
A4: E = {e0} by CARD_1:29;
A5: E = {e} by A2, A3, A4, TARSKI:def 1;
hence A6: not e in the_Edges_of G2 by A2, ZFMISC_1:48; :: thesis: G1 is addEdge of G2,v,e,v
( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ {e} & the_Source_of G1 = (the_Source_of G2) +* (e .--> v) & the_Target_of G1 = (the_Target_of G2) +* (e .--> v) ) by A1, A2, A5, Def5, FUNCOP_1:9;
hence G1 is addEdge of G2,v,e,v by A1, A6, GLIB_006:def 11; :: thesis: verum

end;

given e being object such that A7: ( not e in the_Edges_of G2 & G1 is addEdge of G2,v,e,v ) ; :: thesis: G1 is addLoops of G2,{v}

now :: thesis: ( the_Vertices_of G1 = the_Vertices_of G2 & ex E being set ex f being one-to-one Function st
( 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 ) )

thus the_Vertices_of G1 = the_Vertices_of G2 by A7, GLIB_006:def 11; :: thesis: ex E being set ex f being one-to-one Function st
( 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 )
reconsider f = e .--> v as one-to-one Function ;
take E = {e}; :: thesis: ex f being one-to-one Function st
( 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 )
take f = f; :: thesis: ( 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 )
thus E misses the_Edges_of G2 by A7, ZFMISC_1:50; :: thesis: ( 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 )
thus the_Edges_of G1 = (the_Edges_of G2) \/ E by A7, GLIB_006:def 11; :: thesis: ( dom f = E & rng f = {v} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
thus dom f = E ; :: thesis: ( rng f = {v} & the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
( e is set & v is set ) by TARSKI:1;
hence rng f = {v} by FUNCOP_1:88; :: thesis: ( the_Source_of G1 = (the_Source_of G2) +* f & the_Target_of G1 = (the_Target_of G2) +* f )
thus the_Source_of G1 = (the_Source_of G2) +* f by A7, GLIB_006:def 11; :: thesis: the_Target_of G1 = (the_Target_of G2) +* f
thus the_Target_of G1 = (the_Target_of G2) +* f by A7, GLIB_006:def 11; :: thesis: verum

end;

hence G1 is addLoops of G2,{v} by A7, Def5; :: thesis: verum