theorem :: GLIB_001:65

for G being _Graph
for W being Walk of G
for e, x being object st e Joins W .last() ,x,G holds
( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Element of NAT st n in dom W holds
(W .addEdge e) . n = W . n ) ) by Lm38;