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
for W1 being Walk of G1 holds W1 is Walk of G2
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
for W1 being Walk of G1 holds W1 is Walk of G2
let V be set ; :: thesis: for G1 being addAdjVertexToAll of G,v,V
for G2 being addAdjVertexFromAll of G,v,V
for W1 being Walk of G1 holds W1 is Walk of G2
let G1 be addAdjVertexToAll of G,v,V; :: thesis: for G2 being addAdjVertexFromAll of G,v,V
for W1 being Walk of G1 holds W1 is Walk of G2
let G2 be addAdjVertexFromAll of G,v,V; :: thesis: for W1 being Walk of G1 holds W1 is Walk of G2
let W1 be Walk of G1; :: thesis: W1 is Walk of G2

per cases ( ( V c= the_Vertices_of G & not v in the_Vertices_of G ) or not V c= the_Vertices_of G or v in the_Vertices_of G ) ;

suppose ( V c= the_Vertices_of G & not v in the_Vertices_of G ) ; :: thesis: W1 is Walk of G2

then G2 is reverseEdgeDirections of G1,G1 .edgesOutOf {v} by Th35;
hence W1 is Walk of G2 by Th14; :: thesis: verum

end;

suppose ( not V c= the_Vertices_of G or v in the_Vertices_of G ) ; :: thesis: W1 is Walk of G2

then ( G1 == G & G2 == G ) by Def2, Def3;
hence W1 is Walk of G2 by GLIB_000:85, GLIB_001:179; :: thesis: verum

end;

end;