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

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

let n be Element of NAT ; :: thesis: ( n in dom () iff (2 * n) - 1 in dom W )
hereby :: thesis: ( (2 * n) - 1 in dom W implies n in dom () )
assume A1: n in dom () ; :: 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 () by ;
then 2 * n <= 2 * (len ()) 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 ;
then 2 - 1 <= (2 * n) - 1 by XREAL_1:13;
hence (2 * n) - 1 in dom W by ; :: thesis: verum
end;
assume A5: (2 * n) - 1 in dom W ; :: thesis: n in dom ()
then reconsider 2naa1 = (2 * n) - 1 as Element of NAT ;
1 <= 2naa1 by ;
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 ;
then ((2 * n) - 1) + 1 <= (len W) + 1 by XREAL_1:7;
then 2 * n <= 2 * (len ()) by Def14;
then n <= len () by XREAL_1:68;
hence n in dom () by ; :: thesis: verum