let G be _Graph; :: thesis: for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2
let W be Walk of G; :: thesis: for e, x being set st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2
let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies len (W .addEdge e) = (len W) + 2 )
set W2 = G .walkOf (W .last() ),e,((W .last() ) .adj e);
assume A1: e Joins W .last() ,x,G ; :: thesis: len (W .addEdge e) = (len W) + 2
then reconsider x' = x as Vertex of G by GLIB_000:16;
A2: (W .last() ) .adj e = x' by A1, GLIB_000:69;
then A3: G .walkOf (W .last() ),e,((W .last() ) .adj e) = <*(W .last() ),e,x*> by A1, Def5;
(G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() = W .last() by A1, A2, Lm6;
then (len (W .addEdge e)) + 1 = (len W) + (len (G .walkOf (W .last() ),e,((W .last() ) .adj e))) by Lm9;
then (len (W .addEdge e)) + 1 = (len W) + 3 by A3, FINSEQ_1:62;
hence len (W .addEdge e) = (len W) + 2 ; :: thesis: verum