let G be _Graph; :: thesis: for e, x, y being object st e Joins x,y,G holds
(G .walkOf (x,e,y)) .vertexSeq() = <*x,y*>
let e, x, y be object ; :: 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:45;
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;
((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;
hence (G .walkOf (x,e,y)) .vertexSeq() = <*x,y*> by A2, A3, FINSEQ_1:44; :: thesis: verum