let G be _Graph; :: thesis: for v being object
for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let v be object ; :: thesis: for V being set
for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let V be set ; :: thesis: for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let G1 be addAdjVertexToAll of G,v,V; :: thesis: for G2 being addAdjVertexFromAll of G,v,V st V c= the_Vertices_of G & not v in the_Vertices_of G holds
( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
let G2 be addAdjVertexFromAll of G,v,V; :: thesis: ( V c= the_Vertices_of G & not v in the_Vertices_of G implies ( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} ) )
set E = V --> (the_Edges_of G);
assume A1: ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: ( G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} & G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} )
then A2: ( G1 .edgesOutOf {v} = V --> (the_Edges_of G) & G2 .edgesInto {v} = V --> (the_Edges_of G) ) by Th33, Th34;
A3: ( the_Vertices_of G1 = (the_Vertices_of G) \/ {v} & the_Edges_of G1 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G1 = (the_Source_of G) +* ((V --> (the_Edges_of G)) --> v) & the_Target_of G1 = (the_Target_of G) +* (pr1 (V,{(the_Edges_of G)})) ) by A1, Def2;
A4: ( the_Vertices_of G2 = (the_Vertices_of G) \/ {v} & the_Edges_of G2 = (the_Edges_of G) \/ (V --> (the_Edges_of G)) & the_Source_of G2 = (the_Source_of G) +* (pr1 (V,{(the_Edges_of G)})) & the_Target_of G2 = (the_Target_of G) +* ((V --> (the_Edges_of G)) --> v) ) by A1, Def3;
A5: dom ((V --> (the_Edges_of G)) --> v) = V --> (the_Edges_of G) ;
A6: dom (pr1 (V,{(the_Edges_of G)})) = [:V,{(the_Edges_of G)}:] by FUNCT_3:def 4
.= V --> (the_Edges_of G) by FUNCOP_1:def 2 ;
A9: the_Source_of G2 = (the_Source_of G1) +* ((pr1 (V,{(the_Edges_of G)})) | (V --> (the_Edges_of G))) by A3, A4, A5, A6, FUNCT_4:74
.= (the_Source_of G1) +* ((the_Target_of G1) | (V --> (the_Edges_of G))) by A6, A3 ;
A11: the_Target_of G2 = (the_Target_of G1) +* (((V --> (the_Edges_of G)) --> v) | (V --> (the_Edges_of G))) by A3, A4, A5, A6, FUNCT_4:74
.= (the_Target_of G1) +* ((the_Source_of G1) | (V --> (the_Edges_of G))) by A5, A3 ;
A13: the_Source_of G1 = (the_Source_of G2) +* (((V --> (the_Edges_of G)) --> v) | (V --> (the_Edges_of G))) by A3, A4, A5, A6, FUNCT_4:74
.= (the_Source_of G2) +* ((the_Target_of G2) | (V --> (the_Edges_of G))) by A5, A4 ;
A15: the_Target_of G1 = (the_Target_of G2) +* ((pr1 (V,{(the_Edges_of G)})) | (V --> (the_Edges_of G))) by A3, A4, A5, A6, FUNCT_4:74
.= (the_Target_of G2) +* ((the_Source_of G2) | (V --> (the_Edges_of G))) by A6, A4 ;
thus G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} by A2, A3, A4, A9, A11, Def1; :: thesis: G1 is reverseEdgeDirections of G2,G2 .edgesInto {v}
thus G1 is reverseEdgeDirections of G2,G2 .edgesInto {v} by A2, A3, A4, A13, A15, Def1; :: thesis: verum