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

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

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

then A2: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 ) by GLIB_007:def 1;
E c= (the_Edges_of G1) \/ (G1 .loops()) by A1, XBOOLE_1:44;
then A3: E c= the_Edges_of G1 by XBOOLE_1:12;
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 \ (G1 .loops()))) by A1, GLIB_007:def 1
.= (((the_Target_of G1) | (E /\ (G1 .loops()))) +* (the_Source_of G1)) +* ((the_Target_of G1) | (E \ (G1 .loops()))) by A4, FUNCT_4:19
.= ((the_Source_of G1) +* ((the_Target_of G1) | (E /\ (G1 .loops())))) +* ((the_Target_of G1) | (E \ (G1 .loops()))) by A7, FUNCT_4:34
.= (the_Source_of G1) +* (((the_Target_of G1) | (E /\ (G1 .loops()))) +* ((the_Target_of G1) | (E \ (G1 .loops())))) by FUNCT_4:14
.= (the_Source_of G1) +* ((the_Target_of G1) | ((E /\ (G1 .loops())) \/ (E \ (G1 .loops())))) by FUNCT_4:78
.= (the_Source_of G1) +* ((the_Target_of G1) | E) by XBOOLE_1:51 ;
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 \ (G1 .loops()))) by A1, GLIB_007:def 1
.= (((the_Source_of G1) | (E /\ (G1 .loops()))) +* (the_Target_of G1)) +* ((the_Source_of G1) | (E \ (G1 .loops()))) by A9, FUNCT_4:19
.= ((the_Target_of G1) +* ((the_Source_of G1) | (E /\ (G1 .loops())))) +* ((the_Source_of G1) | (E \ (G1 .loops()))) by A12, FUNCT_4:34
.= (the_Target_of G1) +* (((the_Source_of G1) | (E /\ (G1 .loops()))) +* ((the_Source_of G1) | (E \ (G1 .loops())))) by FUNCT_4:14
.= (the_Target_of G1) +* ((the_Source_of G1) | ((E /\ (G1 .loops())) \/ (E \ (G1 .loops())))) by FUNCT_4:78
.= (the_Target_of G1) +* ((the_Source_of G1) | E) by XBOOLE_1:51 ;
hence G2 is reverseEdgeDirections of G1,E by A3, A2, A8, GLIB_007:def 1; :: thesis: verum

end;

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

A14: not E c= the_Edges_of G1 by A13, XBOOLE_1:1;
G1 == G2 by A13, GLIB_007:def 1;
hence G2 is reverseEdgeDirections of G1,E by A14, GLIB_007:def 1; :: thesis: verum

end;

end;