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() )) )
1 <= len (W .vertexSeq() ) by Th68;
then A1: ( (W .vertexSeq() ) . 1 = W . ((2 * 1) - 1) & (W .vertexSeq() ) . (len (W .vertexSeq() )) = W . ((2 * (len (W .vertexSeq() ))) - 1) ) by Def14;
hence (W .vertexSeq() ) . 1 = W .first() ; :: thesis: W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() ))
(len W) + 1 = 2 * (len (W .vertexSeq() )) by Def14;
hence W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() )) by A1; :: thesis: verum