let G be _Graph; :: thesis: for W being Walk of G

for x being set holds

( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

let W be Walk of G; :: thesis: for x being set holds

( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

let x be set ; :: thesis: ( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

set vs = W .vertexSeq() ;

( n <= len W & W . n = x ) ; :: thesis: x in W .vertices()

then consider n being odd Element of NAT such that

A5: n <= len W and

A6: W . n = x ;

set n1 = n + 1;

reconsider n1 = n + 1 as even Element of NAT ;

set i = n1 div 2;

A7: 2 divides n1 by PEPIN:22;

then A8: 2 * (n1 div 2) = n1 by NAT_D:3;

reconsider i = n1 div 2 as Element of NAT ;

1 <= n by ABIAN:12;

then 1 + 1 <= n1 by XREAL_1:7;

then 2 * 1 <= 2 * i by A7, NAT_D:3;

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

n1 <= (len W) + 1 by A5, XREAL_1:7;

then 2 * i <= 2 * (len (W .vertexSeq())) by A8, Def14;

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

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

(W .vertexSeq()) . i = W . ((2 * i) - 1) by A9, A10, Def14

.= x by A6, A8 ;

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

for x being set holds

( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

let W be Walk of G; :: thesis: for x being set holds

( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

let x be set ; :: thesis: ( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

set vs = W .vertexSeq() ;

hereby :: thesis: ( ex n being odd Element of NAT st

( n <= len W & W . n = x ) implies x in W .vertices() )

assume
ex n being odd Element of NAT st ( n <= len W & W . n = x ) implies x in W .vertices() )

assume
x in W .vertices()
; :: thesis: ex n being odd Element of NAT st

( n <= len W & W . n = x )

then consider i being Nat such that

A1: i in dom (W .vertexSeq()) and

A2: (W .vertexSeq()) . i = x by FINSEQ_2:10;

set n1 = 2 * i;

reconsider n1 = 2 * i as even Nat ;

set n = n1 - 1;

A3: 1 <= i by A1, FINSEQ_3:25;

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

then reconsider n = n1 - 1 as odd Element of NAT by INT_1:5;

take n = n; :: thesis: ( n <= len W & W . n = x )

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

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

then i * 2 <= (len W) + 1 by Def14;

then n1 - 1 <= ((len W) + 1) - 1 by XREAL_1:13;

hence n <= len W ; :: thesis: W . n = x

thus W . n = x by A2, A3, A4, Def14; :: thesis: verum

end;( n <= len W & W . n = x )

then consider i being Nat such that

A1: i in dom (W .vertexSeq()) and

A2: (W .vertexSeq()) . i = x by FINSEQ_2:10;

set n1 = 2 * i;

reconsider n1 = 2 * i as even Nat ;

set n = n1 - 1;

A3: 1 <= i by A1, FINSEQ_3:25;

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

then reconsider n = n1 - 1 as odd Element of NAT by INT_1:5;

take n = n; :: thesis: ( n <= len W & W . n = x )

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

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

then i * 2 <= (len W) + 1 by Def14;

then n1 - 1 <= ((len W) + 1) - 1 by XREAL_1:13;

hence n <= len W ; :: thesis: W . n = x

thus W . n = x by A2, A3, A4, Def14; :: thesis: verum

( n <= len W & W . n = x ) ; :: thesis: x in W .vertices()

then consider n being odd Element of NAT such that

A5: n <= len W and

A6: W . n = x ;

set n1 = n + 1;

reconsider n1 = n + 1 as even Element of NAT ;

set i = n1 div 2;

A7: 2 divides n1 by PEPIN:22;

then A8: 2 * (n1 div 2) = n1 by NAT_D:3;

reconsider i = n1 div 2 as Element of NAT ;

1 <= n by ABIAN:12;

then 1 + 1 <= n1 by XREAL_1:7;

then 2 * 1 <= 2 * i by A7, NAT_D:3;

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

n1 <= (len W) + 1 by A5, XREAL_1:7;

then 2 * i <= 2 * (len (W .vertexSeq())) by A8, Def14;

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

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

(W .vertexSeq()) . i = W . ((2 * i) - 1) by A9, A10, Def14

.= x by A6, A8 ;

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