let G be _Graph; :: thesis: for v being Vertex of G holds (G .walkOf v) .vertexSeq() = <*v*>
let v be Vertex of G; :: thesis: (G .walkOf v) .vertexSeq() = <*v*>
set VS = (G .walkOf v) .vertexSeq() ;
(len (G .walkOf v)) + 1 = 2 * (len ((G .walkOf v) .vertexSeq())) by Def14;
then A1: 1 + 1 = 2 * (len ((G .walkOf v) .vertexSeq())) by Th12;
then ((G .walkOf v) .vertexSeq()) . 1 = (G .walkOf v) . ((2 * 1) - 1) by Def14
.= v by Th12 ;
hence (G .walkOf v) .vertexSeq() = <*v*> by A1, FINSEQ_1:40; :: thesis: verum