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

for n being odd Element of NAT st 1 < n & n <= len W holds

W . (n - 1) in (W .vertexAt n) .edgesInOut()

let W be Walk of G; :: thesis: for n being odd Element of NAT st 1 < n & n <= len W holds

W . (n - 1) in (W .vertexAt n) .edgesInOut()

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W implies W . (n - 1) in (W .vertexAt n) .edgesInOut() )

assume that

A1: 1 < n and

A2: n <= len W ; :: thesis: W . (n - 1) in (W .vertexAt n) .edgesInOut()

reconsider naa1 = n - 1 as even Element of NAT by A1, INT_1:5;

1 + 1 <= n by A1, NAT_1:13;

then A3: (1 + 1) - 1 <= n - 1 by XREAL_1:13;

n - 1 <= (len W) - 0 by A2, XREAL_1:13;

then naa1 in dom W by A3, FINSEQ_3:25;

then consider n5 being odd Element of NAT such that

A4: n5 = naa1 - 1 and

A5: naa1 - 1 in dom W and

naa1 + 1 in dom W and

A6: W . naa1 Joins W . n5,W . (naa1 + 1),G by Lm2;

n5 <= len W by A4, A5, FINSEQ_3:25;

then W . n5 = W .vertexAt n5 by Def8;

then W . (n - 1) Joins W .vertexAt n5,W .vertexAt n,G by A2, A6, Def8;

hence W . (n - 1) in (W .vertexAt n) .edgesInOut() by GLIB_000:14, GLIB_000:62; :: thesis: verum

for n being odd Element of NAT st 1 < n & n <= len W holds

W . (n - 1) in (W .vertexAt n) .edgesInOut()

let W be Walk of G; :: thesis: for n being odd Element of NAT st 1 < n & n <= len W holds

W . (n - 1) in (W .vertexAt n) .edgesInOut()

let n be odd Element of NAT ; :: thesis: ( 1 < n & n <= len W implies W . (n - 1) in (W .vertexAt n) .edgesInOut() )

assume that

A1: 1 < n and

A2: n <= len W ; :: thesis: W . (n - 1) in (W .vertexAt n) .edgesInOut()

reconsider naa1 = n - 1 as even Element of NAT by A1, INT_1:5;

1 + 1 <= n by A1, NAT_1:13;

then A3: (1 + 1) - 1 <= n - 1 by XREAL_1:13;

n - 1 <= (len W) - 0 by A2, XREAL_1:13;

then naa1 in dom W by A3, FINSEQ_3:25;

then consider n5 being odd Element of NAT such that

A4: n5 = naa1 - 1 and

A5: naa1 - 1 in dom W and

naa1 + 1 in dom W and

A6: W . naa1 Joins W . n5,W . (naa1 + 1),G by Lm2;

n5 <= len W by A4, A5, FINSEQ_3:25;

then W . n5 = W .vertexAt n5 by Def8;

then W . (n - 1) Joins W .vertexAt n5,W .vertexAt n,G by A2, A6, Def8;

hence W . (n - 1) in (W .vertexAt n) .edgesInOut() by GLIB_000:14, GLIB_000:62; :: thesis: verum