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

( 1 <= n & n <= len W & W . n = e ) ; :: thesis: e in W .edges()

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 A5, JORDAN12:2, XXREAL_0:1;

then 1 + 1 < n + 1 by XREAL_1:8;

then 2 * 1 <= 2 * i by A8, NAT_1:13;

then A9: 1 <= i by XREAL_1:68;

n < len W by A6, XXREAL_0:1;

then 2 * i < (2 * (len (W .edgeSeq()))) + 1 by A8, Def15;

then 2 * i <= 2 * (len (W .edgeSeq())) by NAT_1:13;

then A10: i <= len (W .edgeSeq()) by XREAL_1:68;

then A11: i in dom (W .edgeSeq()) by A9, FINSEQ_3:25;

(W .edgeSeq()) . i = e by A7, A8, A9, A10, Def15;

hence e in W .edges() by A11, FUNCT_1:def 3; :: thesis: verum

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
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()) 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 A1, FINSEQ_3:25;

then 1 <= i + i by NAT_1:12;

hence 1 <= n ; :: thesis: ( n <= len W & W . n = e )

A4: i <= len (W .edgeSeq()) by A1, FINSEQ_3:25;

then i * 2 <= (len (W .edgeSeq())) * 2 by XREAL_1:64;

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 A2, A3, A4, Def15; :: thesis: verum

end;( 1 <= n & n <= len W & W . n = e )

then consider i being Nat such that

A1: i in dom (W .edgeSeq()) 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 A1, FINSEQ_3:25;

then 1 <= i + i by NAT_1:12;

hence 1 <= n ; :: thesis: ( n <= len W & W . n = e )

A4: i <= len (W .edgeSeq()) by A1, FINSEQ_3:25;

then i * 2 <= (len (W .edgeSeq())) * 2 by XREAL_1:64;

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 A2, A3, A4, Def15; :: thesis: verum

( 1 <= n & n <= len W & W . n = e ) ; :: thesis: e in W .edges()

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 A5, JORDAN12:2, XXREAL_0:1;

then 1 + 1 < n + 1 by XREAL_1:8;

then 2 * 1 <= 2 * i by A8, NAT_1:13;

then A9: 1 <= i by XREAL_1:68;

n < len W by A6, XXREAL_0:1;

then 2 * i < (2 * (len (W .edgeSeq()))) + 1 by A8, Def15;

then 2 * i <= 2 * (len (W .edgeSeq())) by NAT_1:13;

then A10: i <= len (W .edgeSeq()) by XREAL_1:68;

then A11: i in dom (W .edgeSeq()) by A9, FINSEQ_3:25;

(W .edgeSeq()) . i = e by A7, A8, A9, A10, Def15;

hence e in W .edges() by A11, FUNCT_1:def 3; :: thesis: verum