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 Th65;
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