let G1 be loopless _Graph; :: thesis: for V being set
for G2 being addLoops of G1,V
for G3 being removeLoops of G2 holds G1 == G3
let V be set ; :: thesis: for G2 being addLoops of G1,V
for G3 being removeLoops of G2 holds G1 == G3
let G2 be addLoops of G1,V; :: thesis: for G3 being removeLoops of G2 holds G1 == G3
let G3 be removeLoops of G2; :: thesis: G1 == G3

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

suppose A1: V c= the_Vertices_of G1 ; :: thesis: G1 == G3

then A2: the_Vertices_of G1 = the_Vertices_of G2 by Def5
.= the_Vertices_of G3 by GLIB_000:53 ;
A3: the_Edges_of G1 = ((the_Edges_of G1) \/ (G2 .loops())) \ (G2 .loops()) by A1, Th25, XBOOLE_1:88
.= (the_Edges_of G2) \ (G2 .loops()) by A1, Th25
.= the_Edges_of G3 by GLIB_000:53 ;
A4: dom (the_Source_of G1) = the_Edges_of G3 by A3, FUNCT_2:def 1
.= dom (the_Source_of G3) by FUNCT_2:def 1 ;
A5: dom (the_Target_of G1) = the_Edges_of G3 by A3, FUNCT_2:def 1
.= dom (the_Target_of G3) by FUNCT_2:def 1 ;

now :: thesis: for e being object st e in dom (the_Source_of G1) holds
(the_Source_of G1) . e = (the_Source_of G3) . e

let e be object ; :: thesis: ( e in dom (the_Source_of G1) implies (the_Source_of G1) . e = (the_Source_of G3) . e )
assume A6: e in dom (the_Source_of G1) ; :: thesis: (the_Source_of G1) . e = (the_Source_of G3) . e
hence (the_Source_of G1) . e = (the_Source_of G2) . e by GLIB_006:def 9
.= (the_Source_of G3) . e by A3, A6, GLIB_000:def 32 ;
:: thesis: verum

end;

then A7: the_Source_of G1 = the_Source_of G3 by A4, FUNCT_1:2;

now :: thesis: for e being object st e in dom (the_Target_of G1) holds
(the_Target_of G1) . e = (the_Target_of G3) . e

let e be object ; :: thesis: ( e in dom (the_Target_of G1) implies (the_Target_of G1) . e = (the_Target_of G3) . e )
assume A8: e in dom (the_Target_of G1) ; :: thesis: (the_Target_of G1) . e = (the_Target_of G3) . e
hence (the_Target_of G1) . e = (the_Target_of G2) . e by GLIB_006:def 9
.= (the_Target_of G3) . e by A3, A8, GLIB_000:def 32 ;
:: thesis: verum

end;

then the_Target_of G1 = the_Target_of G3 by A5, FUNCT_1:2;
hence G1 == G3 by A2, A3, A7, GLIB_000:def 34; :: thesis: verum

end;

suppose not V c= the_Vertices_of G1 ; :: thesis: G1 == G3

then A9: G1 == G2 by Def5;
then G2 is loopless by GLIB_000:89;
then G2 == G3 by GLIB_009:58;
hence G1 == G3 by A9, GLIB_000:85; :: thesis: verum

end;

end;