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 )

then reconsider 2naa1 = (2 * n) - 1 as Element of NAT ;

1 <= 2naa1 by A5, FINSEQ_3:25;

then 1 + 1 <= ((2 * n) - 1) + 1 by XREAL_1:7;

then 2 * 1 <= 2 * n ;

then A6: 1 <= n by XREAL_1:68;

2naa1 <= len W by A5, FINSEQ_3:25;

then ((2 * n) - 1) + 1 <= (len W) + 1 by XREAL_1:7;

then 2 * n <= 2 * (len (W .vertexSeq())) by Def14;

then n <= len (W .vertexSeq()) by XREAL_1:68;

hence n in dom (W .vertexSeq()) by A6, FINSEQ_3:25; :: thesis: verum

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 A5:
(2 * n) - 1 in dom W
; :: thesis: n in dom (W .vertexSeq())assume A1:
n in dom (W .vertexSeq())
; :: thesis: (2 * n) - 1 in dom W

then A2: 1 <= n by FINSEQ_3:25;

then 1 <= n + n by NAT_1:12;

then A3: (2 * n) - 1 is Element of NAT by INT_1:5;

n <= len (W .vertexSeq()) by A1, FINSEQ_3:25;

then 2 * n <= 2 * (len (W .vertexSeq())) by XREAL_1:64;

then 2 * n <= (len W) + 1 by Def14;

then A4: (2 * n) - 1 <= ((len W) + 1) - 1 by XREAL_1:13;

2 * 1 <= 2 * n by A2, XREAL_1:64;

then 2 - 1 <= (2 * n) - 1 by XREAL_1:13;

hence (2 * n) - 1 in dom W by A4, A3, FINSEQ_3:25; :: thesis: verum

end;then A2: 1 <= n by FINSEQ_3:25;

then 1 <= n + n by NAT_1:12;

then A3: (2 * n) - 1 is Element of NAT by INT_1:5;

n <= len (W .vertexSeq()) by A1, FINSEQ_3:25;

then 2 * n <= 2 * (len (W .vertexSeq())) by XREAL_1:64;

then 2 * n <= (len W) + 1 by Def14;

then A4: (2 * n) - 1 <= ((len W) + 1) - 1 by XREAL_1:13;

2 * 1 <= 2 * n by A2, XREAL_1:64;

then 2 - 1 <= (2 * n) - 1 by XREAL_1:13;

hence (2 * n) - 1 in dom W by A4, A3, FINSEQ_3:25; :: thesis: verum

then reconsider 2naa1 = (2 * n) - 1 as Element of NAT ;

1 <= 2naa1 by A5, FINSEQ_3:25;

then 1 + 1 <= ((2 * n) - 1) + 1 by XREAL_1:7;

then 2 * 1 <= 2 * n ;

then A6: 1 <= n by XREAL_1:68;

2naa1 <= len W by A5, FINSEQ_3:25;

then ((2 * n) - 1) + 1 <= (len W) + 1 by XREAL_1:7;

then 2 * n <= 2 * (len (W .vertexSeq())) by Def14;

then n <= len (W .vertexSeq()) by XREAL_1:68;

hence n in dom (W .vertexSeq()) by A6, FINSEQ_3:25; :: thesis: verum