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