let G be _Graph; :: thesis: for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
W .addEdge e = W ^ <*e,x*>

let W be Walk of G; :: thesis: for e, x being object st e Joins W .last() ,x,G holds
W .addEdge e = W ^ <*e,x*>

let e, x be object ; :: thesis: ( e Joins W .last() ,x,G implies W .addEdge e = W ^ <*e,x*> )
set W1 = G .walkOf ((),e,(() .adj e));
assume A1: e Joins W .last() ,x,G ; :: thesis: W .addEdge e = W ^ <*e,x*>
then reconsider x9 = x as Vertex of G by GLIB_000:13;
A2: (W .last()) .adj e = x9 by ;
then A3: G .walkOf ((),e,(() .adj e)) = <*(),e,x*> by ;
then A4: len (G .walkOf ((),e,(() .adj e))) = 3 by FINSEQ_1:45;
A5: (G .walkOf ((),e,(() .adj e))) . 3 = x by ;
(G .walkOf ((),e,(() .adj e))) . 2 = e by ;
then (2,2) -cut (G .walkOf ((),e,(() .adj e))) = <*e*> by ;
then <*e*> ^ (((2 + 1),3) -cut (G .walkOf ((),e,(() .adj e)))) = ((1 + 1),3) -cut (G .walkOf ((),e,(() .adj e))) by ;
then A6: <*e*> ^ <*x*> = (2,3) -cut (G .walkOf ((),e,(() .adj e))) by ;
W .last() = (G .walkOf ((),e,(() .adj e))) .first() by A1, A2, Lm6;
then W .append (G .walkOf ((),e,(() .adj e))) = W ^' (G .walkOf ((),e,(() .adj e))) by Def10
.= W ^ ((2,(len (G .walkOf ((),e,(() .adj e))))) -cut (G .walkOf ((),e,(() .adj e)))) by FINSEQ_6:def 5
.= W ^ ((2,3) -cut (G .walkOf ((),e,(() .adj e)))) by ;
hence W .addEdge e = W ^ <*e,x*> by ; :: thesis: verum