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 (W .edgeSeq() ) & (W .edgeSeq() ) . i = e ) by FINSEQ_2:11;
set n = 2 * i;
reconsider n = 2 * i as even Element of NAT ;
A2: ( 1 <= i & i <= len (W .edgeSeq() ) ) by A1, FINSEQ_3:27;
take n = n; :: thesis: ( 1 <= n & n <= len W & W . n = e )
1 <= i + i by A2, NAT_1:12;
hence 1 <= n ; :: thesis: ( n <= len W & W . n = e )
i * 2 <= (len (W .edgeSeq() )) * 2 by A2, XREAL_1:66;
then n <= ((len (W .edgeSeq() )) * 2) + 1 by NAT_1:12;
hence n <= len W by Def15; :: thesis: W . n = e
thus W . n = e by A1, A2, Def15; :: thesis: verum

end;

assume ex n being even Element of NAT st
( 1 <= n & n <= len W & W . n = e ) ; :: thesis: e in W .edges()
then consider n being even Element of NAT such that
A3: ( 1 <= n & n <= len W & W . n = e ) ;
set i = n div 2;
2 divides n by PEPIN:22;
then A4: 2 * (n div 2) = n by NAT_D:3;
reconsider i = n div 2 as Element of NAT ;

now

1 < n by A3, JORDAN12:3, XXREAL_0:1;
then 1 + 1 < n + 1 by XREAL_1:10;
then 2 * 1 <= 2 * i by A4, NAT_1:13;
then A5: 1 <= i by XREAL_1:70;
n < len W by A3, XXREAL_0:1;
then 2 * i < (2 * (len (W .edgeSeq() ))) + 1 by A4, Def15;
then 2 * i <= 2 * (len (W .edgeSeq() )) by NAT_1:13;
then A6: i <= len (W .edgeSeq() ) by XREAL_1:70;
hence i in dom (W .edgeSeq() ) by A5, FINSEQ_3:27; :: thesis: (W .edgeSeq() ) . i = e
thus (W .edgeSeq() ) . i = e by A3, A4, A5, A6, Def15; :: thesis: verum

end;

hence e in W .edges() by FUNCT_1:def 5; :: thesis: verum