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