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

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