let G be _Graph; :: thesis: for W being Walk of G holds
( W .first() = (W .vertexSeq() ) . 1 & W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() )) )
let W be Walk of G; :: thesis: ( W .first() = (W .vertexSeq() ) . 1 & W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() )) )
A1: (len W) + 1 = 2 * (len (W .vertexSeq() )) by Def14;
A2: 1 <= len (W .vertexSeq() ) by Th68;
then (W .vertexSeq() ) . 1 = W . ((2 * 1) - 1) by Def14;
hence (W .vertexSeq() ) . 1 = W .first() ; :: thesis: W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() ))
(W .vertexSeq() ) . (len (W .vertexSeq() )) = W . ((2 * (len (W .vertexSeq() ))) - 1) by A2, Def14;
hence W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() )) by A1; :: thesis: verum