let G be _Graph; :: thesis: for W being Walk of G
for n being even Nat st 1 <= n & n <= len W holds
( n div 2 in dom (W .edgeSeq()) & W . n = (W .edgeSeq()) . (n div 2) )
let W be Walk of G; :: thesis: for n being even Nat st 1 <= n & n <= len W holds
( n div 2 in dom (W .edgeSeq()) & W . n = (W .edgeSeq()) . (n div 2) )
let n be even Nat; :: thesis: ( 1 <= n & n <= len W implies ( n div 2 in dom (W .edgeSeq()) & W . n = (W .edgeSeq()) . (n div 2) ) )
assume that
A1: 1 <= n and
A2: n <= len W ; :: thesis: ( n div 2 in dom (W .edgeSeq()) & W . n = (W .edgeSeq()) . (n div 2) )
A3: 2 divides n by PEPIN:22;
then A4: n = 2 * (n div 2) by NAT_D:3;

A5: now :: thesis: n div 2 in dom (W .edgeSeq())

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

now :: thesis: contradiction

per cases ( n div 2 < 0 + 1 or n div 2 > len (W .edgeSeq()) ) by A6, FINSEQ_3:25;

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

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

end;

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

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: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence n div 2 in dom (W .edgeSeq()) ; :: thesis: W . n = (W .edgeSeq()) . (n div 2)
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: verum