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;

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

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())

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

end;now :: thesis: contradictionend;

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

end;

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;then n = 2 * 0 by A3, NAT_D:3;

hence contradiction by A1; :: thesis: verum

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;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

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