let G2 be _Graph; :: thesis:
let v be object ; :: thesis:
let V be set ; :: thesis:
let G1 be addAdjVertexAll of G2,v,V; :: thesis:
assume that
A1: ( V c= the_Vertices_of G2 & not v in the_Vertices_of G2 ) and
A2: for G3 being Component of G2 ex w being Vertex of G3 st w in V ; :: thesis:
A3: for u being Vertex of G1 st u <> v holds
ex W1 being Walk of G1 st W1 is_Walk_from u,v

let u be Vertex of G1; :: thesis:
assume u <> v ; :: thesis:
then A4: not u in {v} by TARSKI:def 1;
the_Vertices_of G1 = (the_Vertices_of G2) \/ {v} by A1, Def4;
then u in the_Vertices_of G2 by A4, XBOOLE_0:def 3;
then reconsider u1 = u as Vertex of G2 ;
reconsider G3 = the inducedSubgraph of G2,(G2 .reachableFrom u1) as Component of G2 ;
consider w being Vertex of G3 such that
A5: w in V by A2;
the_Vertices_of G3 = G2 .reachableFrom u1 by GLIB_000:def 37;
then w in G2 .reachableFrom u1 ;
then consider W2 being Walk of G2 such that
A6: W2 is_Walk_from u1,w by GLIB_002:def 5;
reconsider W3 = W2 as Walk of G1 by GLIB_006:75;
A7: W3 is_Walk_from u,w by A6, GLIB_001:19;
consider E being set such that
( card V = card E & E misses the_Edges_of G2 & the_Edges_of G1 = (the_Edges_of G2) \/ E ) and
A8: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,G1 & ( for e2 being object st e2 Joins v1,v,G1 holds
e1 = e2 ) ) by A1, Def4;
consider e1 being object such that
A9: ( e1 in E & e1 Joins w,v,G1 ) and
for e2 being object st e2 Joins w,v,G1 holds
e1 = e2 by A8, A5;
take W3 .addEdge e1 ; :: thesis:
( W3 .first() = u & W3 .last() = w ) by A7, GLIB_001:def 23;
hence W3 .addEdge e1 is_Walk_from u,v by A9, GLIB_001:63; :: thesis:

end;

for u, w being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u,w

let u, w be Vertex of G1; :: thesis:

end;

end;

end;

end;