let G be _Graph; :: thesis:
let W be Walk of G; :: thesis:
let n be even Nat; :: thesis:
assume that
A1: 1 <= n and
A2: n <= len W ; :: thesis:
A3: 2 divides n by PEPIN:22;
then A4: n = 2 * (n div 2) by NAT_D:3;

A5: now :: thesis:

assume A6: not n div 2 in dom (W .edgeSeq()) ; :: thesis:

per cases by A6, FINSEQ_3:25;

suppose n div 2 < 0 + 1 ; :: thesis:

then n div 2 = 0 by NAT_1:13;
then n = 2 * 0 by A3, NAT_D:3;
hence contradiction by A1; :: thesis:

end;

suppose n div 2 > len (W .edgeSeq()) ; :: thesis:

then 2 * (n div 2) > 2 * (len (W .edgeSeq())) by XREAL_1:68;
then n + 1 > (2 * (len (W .edgeSeq()))) + 1 by A4, XREAL_1:8;
then n + 1 > len W by Def15;
then n >= len W by NAT_1:13;
hence contradiction by A2, XXREAL_0:1; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

hence n div 2 in dom (W .edgeSeq()) ; :: thesis:
A7: n div 2 <= len (W .edgeSeq()) by A5, FINSEQ_3:25;
1 <= n div 2 by A5, FINSEQ_3:25;
hence W . n = (W .edgeSeq()) . (n div 2) by A4, A7, Def15; :: thesis: