let G be _Graph; :: thesis: for e, x, y being set st e Joins x,y,G holds
(G .walkOf x,e,y) .vertexSeq() = <*x,y*>
let e, x, y be set ; :: thesis: ( e Joins x,y,G implies (G .walkOf x,e,y) .vertexSeq() = <*x,y*> )
set W = G .walkOf x,e,y;
assume e Joins x,y,G ; :: thesis: (G .walkOf x,e,y) .vertexSeq() = <*x,y*>
then A1: G .walkOf x,e,y = <*x,e,y*> by Def5;
(len (G .walkOf x,e,y)) + 1 = 2 * (len ((G .walkOf x,e,y) .vertexSeq() )) by Def14;
then A2: 3 + 1 = 2 * (len ((G .walkOf x,e,y) .vertexSeq() )) by A1, FINSEQ_1:62;
then ((G .walkOf x,e,y) .vertexSeq() ) . 2 = (G .walkOf x,e,y) . ((2 * 2) - 1) by Def14;
then A3: ((G .walkOf x,e,y) .vertexSeq() ) . 2 = y by A1, FINSEQ_1:62;
((G .walkOf x,e,y) .vertexSeq() ) . 1 = (G .walkOf x,e,y) . ((2 * 1) - 1) by A2, Def14;
then ((G .walkOf x,e,y) .vertexSeq() ) . 1 = x by A1, FINSEQ_1:62;
hence (G .walkOf x,e,y) .vertexSeq() = <*x,y*> by A2, A3, FINSEQ_1:61; :: thesis: verum