let G be _Graph; :: thesis: 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))

let W be Walk of G; :: thesis: 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))

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n < len W implies (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2)) )

set W1 = W .cut (m,n);

set e = W . (n + 1);

assume that

A1: m <= n and

A2: n < len W ; :: thesis: (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))

A3: n + 2 <= len W by A2, Th1;

A4: (W .cut (m,n)) .last() = W . n by A1, A2, Lm16;

then W . (n + 1) Joins (W .cut (m,n)) .last() ,W . (n + 2),G by A2, Def3;

then W . (n + 1) Joins (W .cut (m,n)) .last() ,W .vertexAt (n + 2),G by A3, Def8;

then ((W .cut (m,n)) .last()) .adj (W . (n + 1)) = W .vertexAt (n + 2) by GLIB_000:66;

then ((W .cut (m,n)) .last()) .adj (W . (n + 1)) = W . (n + 2) by A3, Def8;

then A5: G .walkOf (((W .cut (m,n)) .last()),(W . (n + 1)),(((W .cut (m,n)) .last()) .adj (W . (n + 1)))) = W .cut (n,(n + 2)) by A2, A4, Th38;

n <= n + 2 by Th1;

hence (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2)) by A1, A3, A5, Lm17; :: thesis: verum

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))

let W be Walk of G; :: thesis: 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))

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n < len W implies (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2)) )

set W1 = W .cut (m,n);

set e = W . (n + 1);

assume that

A1: m <= n and

A2: n < len W ; :: thesis: (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))

A3: n + 2 <= len W by A2, Th1;

A4: (W .cut (m,n)) .last() = W . n by A1, A2, Lm16;

then W . (n + 1) Joins (W .cut (m,n)) .last() ,W . (n + 2),G by A2, Def3;

then W . (n + 1) Joins (W .cut (m,n)) .last() ,W .vertexAt (n + 2),G by A3, Def8;

then ((W .cut (m,n)) .last()) .adj (W . (n + 1)) = W .vertexAt (n + 2) by GLIB_000:66;

then ((W .cut (m,n)) .last()) .adj (W . (n + 1)) = W . (n + 2) by A3, Def8;

then A5: G .walkOf (((W .cut (m,n)) .last()),(W . (n + 1)),(((W .cut (m,n)) .last()) .adj (W . (n + 1)))) = W .cut (n,(n + 2)) by A2, A4, Th38;

n <= n + 2 by Th1;

hence (W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2)) by A1, A3, A5, Lm17; :: thesis: verum