let G be _Graph; :: thesis: for W being Walk of G

for n being Nat holds

( n in dom (W .edgeSeq()) iff 2 * n in dom W )

let W be Walk of G; :: thesis: for n being Nat holds

( n in dom (W .edgeSeq()) iff 2 * n in dom W )

let n be Nat; :: thesis: ( n in dom (W .edgeSeq()) iff 2 * n in dom W )

then A4: 2 * n <= len W by FINSEQ_3:25;

1 <= 2 * n by A3, FINSEQ_3:25;

then (2 * n) div 2 in dom (W .edgeSeq()) by A4, Lm40;

hence n in dom (W .edgeSeq()) by NAT_D:18; :: thesis: verum

for n being Nat holds

( n in dom (W .edgeSeq()) iff 2 * n in dom W )

let W be Walk of G; :: thesis: for n being Nat holds

( n in dom (W .edgeSeq()) iff 2 * n in dom W )

let n be 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 A3:
2 * n in dom W
; :: thesis: n in dom (W .edgeSeq())assume A1:
n in dom (W .edgeSeq())
; :: thesis: 2 * n in dom W

then n <= len (W .edgeSeq()) by FINSEQ_3:25;

then 2 * n <= (len (W .edgeSeq())) * 2 by NAT_1:4;

then 2 * n <= ((len (W .edgeSeq())) * 2) + 1 by NAT_1:12;

then A2: 2 * n <= len W by Def15;

1 <= n by A1, FINSEQ_3:25;

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

hence 2 * n in dom W by A2, FINSEQ_3:25; :: thesis: verum

end;then n <= len (W .edgeSeq()) by FINSEQ_3:25;

then 2 * n <= (len (W .edgeSeq())) * 2 by NAT_1:4;

then 2 * n <= ((len (W .edgeSeq())) * 2) + 1 by NAT_1:12;

then A2: 2 * n <= len W by Def15;

1 <= n by A1, FINSEQ_3:25;

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

hence 2 * n in dom W by A2, FINSEQ_3:25; :: thesis: verum

then A4: 2 * n <= len W by FINSEQ_3:25;

1 <= 2 * n by A3, FINSEQ_3:25;

then (2 * n) div 2 in dom (W .edgeSeq()) by A4, Lm40;

hence n in dom (W .edgeSeq()) by NAT_D:18; :: thesis: verum