let G be _Graph; :: thesis: for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) )

let W be Walk of G; :: thesis: for e being set holds
( e in W .edges() iff ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) )

let e be set ; :: thesis: ( e in W .edges() iff ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) )

set es = W .edgeSeq() ;
hereby :: thesis: ( ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) implies e in W .edges() )
assume e in W .edges() ; :: thesis: ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e )

then consider i being Nat such that
A1: i in dom () and
A2: (W .edgeSeq()) . i = e by FINSEQ_2:10;
set n = 2 * i;
reconsider n = 2 * i as even Element of NAT by ORDINAL1:def 12;
take n = n; :: thesis: ( 1 <= n & n <= len W & W . n = e )
A3: 1 <= i by ;
then 1 <= i + i by NAT_1:12;
hence 1 <= n ; :: thesis: ( n <= len W & W . n = e )
A4: i <= len () by ;
then i * 2 <= (len ()) * 2 by XREAL_1:64;
then n <= ((len ()) * 2) + 1 by NAT_1:12;
hence n <= len W by Def15; :: thesis: W . n = e
thus W . n = e by A2, A3, A4, Def15; :: thesis: verum
end;
assume ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) ; :: thesis:
then consider n being even Element of NAT such that
A5: 1 <= n and
A6: n <= len W and
A7: W . n = e ;
set i = n div 2;
2 divides n by PEPIN:22;
then A8: 2 * (n div 2) = n by NAT_D:3;
reconsider i = n div 2 as Element of NAT ;
1 < n by ;
then 1 + 1 < n + 1 by XREAL_1:8;
then 2 * 1 <= 2 * i by ;
then A9: 1 <= i by XREAL_1:68;
n < len W by ;
then 2 * i < (2 * (len ())) + 1 by ;
then 2 * i <= 2 * (len ()) by NAT_1:13;
then A10: i <= len () by XREAL_1:68;
then A11: i in dom () by ;
(W .edgeSeq()) . i = e by A7, A8, A9, A10, Def15;
hence e in W .edges() by ; :: thesis: verum