let G be _Graph; :: thesis: for W being Walk of G holds len (W .vertexSeq()) = (W .length()) + 1
let W be Walk of G; :: thesis: len (W .vertexSeq()) = (W .length()) + 1
2 * (len (W .vertexSeq())) = (len W) + 1 by GLIB_001:def 14
.= ((2 * (W .length())) + 1) + 1 by GLIB_001:112
.= 2 * ((W .length()) + 1) ;
hence len (W .vertexSeq()) = (W .length()) + 1 ; :: thesis: verum