theorem :: GLIB_001:79

for G being _Graph
for W being Walk of G
for n being Element of NAT st n in dom (W .edgeSeq()) holds
(W .edgeSeq()) . n in the_Edges_of G