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 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;
W .last() = (G .walkOf (W .last() ),e,((W .last() ) .adj e)) .first() by A1, A2, Lm6;
then A4: 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 ;
A5: ( len (G .walkOf (W .last() ),e,((W .last() ) .adj e)) = 3 & (G .walkOf (W .last() ),e,((W .last() ) .adj e)) . 2 = e & (G .walkOf (W .last() ),e,((W .last() ) .adj e)) . 3 = x ) by A3, FINSEQ_1:62;
then ( 2,2 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e)) = <*e*> & 3,3 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e)) = <*x*> ) by 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 A5, GRAPH_2:8;
then <*e*> ^ <*x*> = 2,3 -cut (G .walkOf (W .last() ),e,((W .last() ) .adj e)) by A5, GRAPH_2:6;
hence W .addEdge e = W ^ <*e,x*> by A4, FINSEQ_1:def 9; :: thesis: verum