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 ((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:13;
A2: (W .last()) .adj e = x9 by A1, GLIB_000:66;
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:45;
A5: (G .walkOf ((W .last()),e,((W .last()) .adj e))) . 3 = x by A3;
(G .walkOf ((W .last()),e,((W .last()) .adj e))) . 2 = e by A3;
then (2,2) -cut (G .walkOf ((W .last()),e,((W .last()) .adj e))) = <*e*> by A4, FINSEQ_6:132;
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, FINSEQ_6:134;
then A6: <*e*> ^ <*x*> = (2,3) -cut (G .walkOf ((W .last()),e,((W .last()) .adj e))) by A4, A5, FINSEQ_6:132;
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 FINSEQ_6:def 5
.= W ^ ((2,3) -cut (G .walkOf ((W .last()),e,((W .last()) .adj e)))) by A3, FINSEQ_1:45 ;
hence W .addEdge e = W ^ <*e,x*> by A6, FINSEQ_1:def 9; :: thesis: verum