let G be _Graph; :: thesis: for W being Walk of G
for e, x being set 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 set st e Joins W .last() ,x,G holds
W .addEdge e = W ^ <*e,x*>
let e, x be set ; :: thesis: ( e Joins W .last() ,x,G implies W .addEdge e = W ^ <*e,x*> )
set W1 = G .walkOf (W .last() ),e,((W .last() ) .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:16;
A2: (W .last() ) .adj e = x9 by A1, GLIB_000:69;
then A3: G .walkOf (W .last() ),e,((W .last() ) .adj e) = <*(W .last() ),e,x*> by A1, Def5;
then A4: len (G .walkOf (W .last() ),e,((W .last() ) .adj e)) = 3 by FINSEQ_1:62;
A5: (G .walkOf (W .last() ),e,((W .last() ) .adj e)) . 3 = x by A3, FINSEQ_1:62;
(G .walkOf (W .last() ),e,((W .last() ) .adj e)) . 2 = e by A3, FINSEQ_1:62;
then 2,2 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e)) = <*e*> by A4, GRAPH_2:6;
then <*e*> ^ ((2 + 1),3 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e))) = (1 + 1),3 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e)) by A4, GRAPH_2:8;
then A6: <*e*> ^ <*x*> = 2,3 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e)) by A4, A5, GRAPH_2:6;
W .last() = (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() by A1, A2, Lm6;
then W .append (G .walkOf (W .last() ),e,((W .last() ) .adj e)) = W ^' (G .walkOf (W .last() ),e,((W .last() ) .adj e)) by Def10
.= W ^ (2,(len (G .walkOf (W .last() ),e,((W .last() ) .adj e))) -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e))) by GRAPH_2:def 2
.= W ^ (2,3 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e))) by A3, FINSEQ_1:62 ;
hence W .addEdge e = W ^ <*e,x*> by A6, FINSEQ_1:def 9; :: thesis: verum