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:69;
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, Th41;
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