theorem Th39: :: GLIB_001:41

for G being _Graph
for W being Walk of G
for m, n being odd Element of NAT st m <= n & n < len W holds
(W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))