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

hereby :: thesis: ( 2 * n in dom W implies n in dom (W .edgeSeq() ) )

assume n in dom (W .edgeSeq() ) ; :: thesis: 2 * n in dom W
then A1: ( 1 <= n & n <= len (W .edgeSeq() ) ) by FINSEQ_3:27;
then A2: 1 <= n + n by NAT_1:12;
2 * n <= (len (W .edgeSeq() )) * 2 by A1, NAT_1:4;
then 2 * n <= ((len (W .edgeSeq() )) * 2) + 1 by NAT_1:12;
then 2 * n <= len W by Def15;
hence 2 * n in dom W by A2, FINSEQ_3:27; :: thesis: verum

end;

assume 2 * n in dom W ; :: thesis: n in dom (W .edgeSeq() )
then ( 1 <= 2 * n & 2 * n <= len W ) by FINSEQ_3:27;
then (2 * n) div 2 in dom (W .edgeSeq() ) by Lm40;
hence n in dom (W .edgeSeq() ) by NAT_D:20; :: thesis: verum