theorem :: GLIB_001:71

for G being _Graph
for W being Walk of G holds
( W .first() = (W .vertexSeq()) . 1 & W .last() = (W .vertexSeq()) . (len (W .vertexSeq())) )