let G1 be _Graph; :: thesis: for E being set
for G2 being reverseEdgeDirections of G1,E holds G2 is reverseEdgeDirections of G1,E \ (G1 .loops())
let E be set ; :: thesis: for G2 being reverseEdgeDirections of G1,E holds G2 is reverseEdgeDirections of G1,E \ (G1 .loops())
let G2 be reverseEdgeDirections of G1,E; :: thesis: G2 is reverseEdgeDirections of G1,E \ (G1 .loops())

per cases ( E c= the_Edges_of G1 or not E c= the_Edges_of G1 ) ;

suppose A1: E c= the_Edges_of G1 ; :: thesis: G2 is reverseEdgeDirections of G1,E \ (G1 .loops())

then A2: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_007:def 1;
A3: E \ (G1 .loops()) c= the_Edges_of G1 by A1, XBOOLE_1:1;
set S = the_Source_of G1;
set T = the_Target_of G1;
dom ((the_Target_of G1) | (E /\ (G1 .loops()))) c= dom (the_Target_of G1) by RELAT_1:60;
then dom ((the_Target_of G1) | (E /\ (G1 .loops()))) c= the_Edges_of G1 by FUNCT_2:def 1;
then A4: dom ((the_Target_of G1) | (E /\ (G1 .loops()))) c= dom (the_Source_of G1) by FUNCT_2:def 1;

now :: thesis: for x being object st x in (dom (the_Source_of G1)) /\ (dom ((the_Target_of G1) | (E /\ (G1 .loops())))) holds
(the_Source_of G1) . x = ((the_Target_of G1) | (E /\ (G1 .loops()))) . x

let x be object ; :: thesis: ( x in (dom (the_Source_of G1)) /\ (dom ((the_Target_of G1) | (E /\ (G1 .loops())))) implies (the_Source_of G1) . x = ((the_Target_of G1) | (E /\ (G1 .loops()))) . x )
assume x in (dom (the_Source_of G1)) /\ (dom ((the_Target_of G1) | (E /\ (G1 .loops())))) ; :: thesis: (the_Source_of G1) . x = ((the_Target_of G1) | (E /\ (G1 .loops()))) . x
then A5: x in dom ((the_Target_of G1) | (E /\ (G1 .loops()))) by A4, XBOOLE_1:28;
then x in G1 .loops() by XBOOLE_0:def 4;
then A6: x in dom ((the_Source_of G1) /\ (the_Target_of G1)) by Th67;
thus (the_Source_of G1) . x = ((the_Source_of G1) /\ (the_Target_of G1)) . x by A6, GRFUNC_1:11
.= (the_Target_of G1) . x by A6, GRFUNC_1:11
.= ((the_Target_of G1) | (E /\ (G1 .loops()))) . x by A5, FUNCT_1:47 ; :: thesis: verum

end;

then A7: the_Source_of G1 tolerates (the_Target_of G1) | (E /\ (G1 .loops())) by PARTFUN1:def 4;
A8: the_Source_of G2 = (the_Source_of G1) +* ((the_Target_of G1) | E) by A1, GLIB_007:def 1
.= (the_Source_of G1) +* ((the_Target_of G1) | ((E /\ (G1 .loops())) \/ (E \ (G1 .loops())))) by XBOOLE_1:51
.= (the_Source_of G1) +* (((the_Target_of G1) | (E /\ (G1 .loops()))) +* ((the_Target_of G1) | (E \ (G1 .loops())))) by FUNCT_4:78
.= ((the_Source_of G1) +* ((the_Target_of G1) | (E /\ (G1 .loops())))) +* ((the_Target_of G1) | (E \ (G1 .loops()))) by FUNCT_4:14
.= (((the_Target_of G1) | (E /\ (G1 .loops()))) +* (the_Source_of G1)) +* ((the_Target_of G1) | (E \ (G1 .loops()))) by A7, FUNCT_4:34
.= (the_Source_of G1) +* ((the_Target_of G1) | (E \ (G1 .loops()))) by A4, FUNCT_4:19 ;
dom ((the_Source_of G1) | (E /\ (G1 .loops()))) c= dom (the_Source_of G1) by RELAT_1:60;
then dom ((the_Source_of G1) | (E /\ (G1 .loops()))) c= the_Edges_of G1 by FUNCT_2:def 1;
then A9: dom ((the_Source_of G1) | (E /\ (G1 .loops()))) c= dom (the_Target_of G1) by FUNCT_2:def 1;

now :: thesis: for x being object st x in (dom (the_Target_of G1)) /\ (dom ((the_Source_of G1) | (E /\ (G1 .loops())))) holds
(the_Target_of G1) . x = ((the_Source_of G1) | (E /\ (G1 .loops()))) . x

let x be object ; :: thesis: ( x in (dom (the_Target_of G1)) /\ (dom ((the_Source_of G1) | (E /\ (G1 .loops())))) implies (the_Target_of G1) . x = ((the_Source_of G1) | (E /\ (G1 .loops()))) . x )
assume x in (dom (the_Target_of G1)) /\ (dom ((the_Source_of G1) | (E /\ (G1 .loops())))) ; :: thesis: (the_Target_of G1) . x = ((the_Source_of G1) | (E /\ (G1 .loops()))) . x
then A10: x in dom ((the_Source_of G1) | (E /\ (G1 .loops()))) by A9, XBOOLE_1:28;
then x in G1 .loops() by XBOOLE_0:def 4;
then A11: x in dom ((the_Source_of G1) /\ (the_Target_of G1)) by Th67;
thus (the_Target_of G1) . x = ((the_Source_of G1) /\ (the_Target_of G1)) . x by A11, GRFUNC_1:11
.= (the_Source_of G1) . x by A11, GRFUNC_1:11
.= ((the_Source_of G1) | (E /\ (G1 .loops()))) . x by A10, FUNCT_1:47 ; :: thesis: verum

end;

then A12: the_Target_of G1 tolerates (the_Source_of G1) | (E /\ (G1 .loops())) by PARTFUN1:def 4;
the_Target_of G2 = (the_Target_of G1) +* ((the_Source_of G1) | E) by A1, GLIB_007:def 1
.= (the_Target_of G1) +* ((the_Source_of G1) | ((E /\ (G1 .loops())) \/ (E \ (G1 .loops())))) by XBOOLE_1:51
.= (the_Target_of G1) +* (((the_Source_of G1) | (E /\ (G1 .loops()))) +* ((the_Source_of G1) | (E \ (G1 .loops())))) by FUNCT_4:78
.= ((the_Target_of G1) +* ((the_Source_of G1) | (E /\ (G1 .loops())))) +* ((the_Source_of G1) | (E \ (G1 .loops()))) by FUNCT_4:14
.= (((the_Source_of G1) | (E /\ (G1 .loops()))) +* (the_Target_of G1)) +* ((the_Source_of G1) | (E \ (G1 .loops()))) by A12, FUNCT_4:34
.= (the_Target_of G1) +* ((the_Source_of G1) | (E \ (G1 .loops()))) by A9, FUNCT_4:19 ;
hence G2 is reverseEdgeDirections of G1,E \ (G1 .loops()) by A2, A3, A8, GLIB_007:def 1; :: thesis: verum

end;

suppose A13: not E c= the_Edges_of G1 ; :: thesis: G2 is reverseEdgeDirections of G1,E \ (G1 .loops())

then A14: G1 == G2 by GLIB_007:def 1;
consider e being object such that
A15: ( e in E & not e in the_Edges_of G1 ) by A13, TARSKI:def 3;
not e in G1 .loops() by A15;
then e in E \ (G1 .loops()) by A15, XBOOLE_0:def 5;
then not E \ (G1 .loops()) c= the_Edges_of G1 by A15;
hence G2 is reverseEdgeDirections of G1,E \ (G1 .loops()) by A14, GLIB_007:def 1; :: thesis: verum

end;

end;