theorem :: GLIB_001:78

for G being _Graph
for W being Walk of G
for n being Element of NAT holds
( n in dom (W .edgeSeq()) iff 2 * n in dom W ) by Lm41;