let G1 be _Graph; :: thesis: for e being set
for G2 being removeEdge of G1,e st e in the_Edges_of G1 holds
G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e
let e be set ; :: thesis: for G2 being removeEdge of G1,e st e in the_Edges_of G1 holds
G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e
let G2 be removeEdge of G1,e; :: thesis: ( e in the_Edges_of G1 implies G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e )
assume A1: e in the_Edges_of G1 ; :: thesis: G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e
set u = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
A2: G1 is Supergraph of G2 by GLIB_006:57;
A3: the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:51;
A4: the_Edges_of G1 = ((the_Edges_of G1) \ {e}) \/ {e} by A1, ZFMISC_1:116
.= (the_Edges_of G2) \/ {e} by GLIB_000:51 ;
A5: dom (the_Source_of G1) = the_Edges_of G1 by FUNCT_2:def 1
.= (dom (the_Source_of G2)) \/ (dom ({e} --> ((the_Source_of G1) . e))) by A4, FUNCT_2:def 1
.= (dom (the_Source_of G2)) \/ (dom (e .--> ((the_Source_of G1) . e))) by FUNCOP_1:def 9
.= dom ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) by FUNCT_4:def 1 ;
for e0 being object st e0 in dom (the_Source_of G1) holds
(the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0

proof

let e0 be object ; :: thesis: ( e0 in dom (the_Source_of G1) implies (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0 )
assume A6: e0 in dom (the_Source_of G1) ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0

per cases ( e0 = e or e0 <> e ) ;

suppose e0 = e ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0

hence (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0 by FUNCT_4:113; :: thesis: verum

end;

suppose A7: e0 <> e ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0

then not e0 in {e} by TARSKI:def 1;
then e0 in (the_Edges_of G1) \ {e} by A6, XBOOLE_0:def 5;
then e0 in the_Edges_of G2 by GLIB_000:51;
hence (the_Source_of G1) . e0 = (the_Source_of G2) . e0 by GLIB_000:def 32
.= ((the_Source_of G2) +* (e .--> ((the_Source_of G1) . e))) . e0 by A7, FUNCT_4:83 ;
:: thesis: verum

end;

end;

end;

then A8: the_Source_of G1 = (the_Source_of G2) +* (e .--> ((the_Source_of G1) . e)) by A5, FUNCT_1:2;
A9: dom (the_Target_of G1) = the_Edges_of G1 by FUNCT_2:def 1
.= (dom (the_Target_of G2)) \/ (dom ({e} --> ((the_Target_of G1) . e))) by A4, FUNCT_2:def 1
.= (dom (the_Target_of G2)) \/ (dom (e .--> ((the_Target_of G1) . e))) by FUNCOP_1:def 9
.= dom ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) by FUNCT_4:def 1 ;
for e0 being object st e0 in dom (the_Target_of G1) holds
(the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0

proof

let e0 be object ; :: thesis: ( e0 in dom (the_Target_of G1) implies (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0 )
assume A10: e0 in dom (the_Target_of G1) ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0

per cases ( e0 = e or e0 <> e ) ;

suppose e0 = e ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0

hence (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0 by FUNCT_4:113; :: thesis: verum

end;

suppose A11: e0 <> e ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0

then not e0 in {e} by TARSKI:def 1;
then e0 in (the_Edges_of G1) \ {e} by A10, XBOOLE_0:def 5;
then e0 in the_Edges_of G2 by GLIB_000:51;
hence (the_Target_of G1) . e0 = (the_Target_of G2) . e0 by GLIB_000:def 32
.= ((the_Target_of G2) +* (e .--> ((the_Target_of G1) . e))) . e0 by A11, FUNCT_4:83 ;
:: thesis: verum

end;

end;

end;

then A12: the_Target_of G1 = (the_Target_of G2) +* (e .--> ((the_Target_of G1) . e)) by A9, FUNCT_1:2;
A13: ( (the_Source_of G1) . e in the_Vertices_of G2 & (the_Target_of G1) . e in the_Vertices_of G2 ) by A1, A3, FUNCT_2:5;
e in {e} by TARSKI:def 1;
then not e in (the_Edges_of G1) \ {e} by XBOOLE_0:def 5;
then not e in the_Edges_of G2 by GLIB_000:51;
hence G1 is addEdge of G2,(the_Source_of G1) . e,e,(the_Target_of G1) . e by A2, A3, A4, A8, A12, A13, GLIB_006:def 11; :: thesis: verum