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

for n being even Element of NAT st n in dom W holds

W . n in the_Edges_of G

let W be Walk of G; :: thesis: for n being even Element of NAT st n in dom W holds

W . n in the_Edges_of G

let n be even Element of NAT ; :: thesis: ( n in dom W implies W . n in the_Edges_of G )

assume A1: n in dom W ; :: thesis: W . n in the_Edges_of G

then 1 <= n by FINSEQ_3:25;

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

n <= len W by A1, FINSEQ_3:25;

then naa1 < (len W) - 0 by XREAL_1:15;

then W . (naa1 + 1) Joins W . naa1,W . (naa1 + 2),G by Def3;

hence W . n in the_Edges_of G by GLIB_000:def 13; :: thesis: verum

for n being even Element of NAT st n in dom W holds

W . n in the_Edges_of G

let W be Walk of G; :: thesis: for n being even Element of NAT st n in dom W holds

W . n in the_Edges_of G

let n be even Element of NAT ; :: thesis: ( n in dom W implies W . n in the_Edges_of G )

assume A1: n in dom W ; :: thesis: W . n in the_Edges_of G

then 1 <= n by FINSEQ_3:25;

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

n <= len W by A1, FINSEQ_3:25;

then naa1 < (len W) - 0 by XREAL_1:15;

then W . (naa1 + 1) Joins W . naa1,W . (naa1 + 2),G by Def3;

hence W . n in the_Edges_of G by GLIB_000:def 13; :: thesis: verum