let G be _Graph; :: thesis: for W being Walk of G
for n being Element of NAT holds
( n in dom (W .vertexSeq() ) iff (2 * n) - 1 in dom W )
let W be Walk of G; :: thesis: for n being Element of NAT holds
( n in dom (W .vertexSeq() ) iff (2 * n) - 1 in dom W )
let n be Element of NAT ; :: thesis: ( n in dom (W .vertexSeq() ) iff (2 * n) - 1 in dom W )

hereby :: thesis: ( (2 * n) - 1 in dom W implies n in dom (W .vertexSeq() ) )

assume n in dom (W .vertexSeq() ) ; :: thesis: (2 * n) - 1 in dom W
then A1: ( 1 <= n & n <= len (W .vertexSeq() ) ) by FINSEQ_3:27;
then 2 * n <= 2 * (len (W .vertexSeq() )) by XREAL_1:66;
then 2 * n <= (len W) + 1 by Def14;
then A2: (2 * n) - 1 <= ((len W) + 1) - 1 by XREAL_1:15;
2 * 1 <= 2 * n by A1, XREAL_1:66;
then A3: 2 - 1 <= (2 * n) - 1 by XREAL_1:15;
1 <= n + n by A1, NAT_1:12;
then (2 * n) - 1 is Element of NAT by INT_1:18;
hence (2 * n) - 1 in dom W by A2, A3, FINSEQ_3:27; :: thesis: verum

end;

assume A4: (2 * n) - 1 in dom W ; :: thesis: n in dom (W .vertexSeq() )
then reconsider 2naa1 = (2 * n) - 1 as Element of NAT ;
( 1 <= 2naa1 & 2naa1 <= len W ) by A4, FINSEQ_3:27;
then A5: ( 1 + 1 <= ((2 * n) - 1) + 1 & ((2 * n) - 1) + 1 <= (len W) + 1 ) by XREAL_1:9;
then A6: ( 2 * 1 <= 2 * n & 2 * n <= (len W) + 1 ) ;
2 * n <= 2 * (len (W .vertexSeq() )) by A5, Def14;
then ( 1 <= n & n <= len (W .vertexSeq() ) ) by A6, XREAL_1:70;
hence n in dom (W .vertexSeq() ) by FINSEQ_3:27; :: thesis: verum