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
( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) )

let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W holds
( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) )

let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W implies ( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) ) )

set W2 = W .cut (m,n);
assume that
A1: m <= n and
A2: n <= len W ; :: thesis: ( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) ) )

A3: 1 <= m by ABIAN:12;
A4: W .cut (m,n) = (m,n) -cut W by ;
hence A5: (len (W .cut (m,n))) + m = n + 1 by ; :: thesis: for i being Element of NAT st i < len (W .cut (m,n)) holds
( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W )

let i be Element of NAT ; :: thesis: ( i < len (W .cut (m,n)) implies ( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W ) )
assume A6: i < len (W .cut (m,n)) ; :: thesis: ( (W .cut (m,n)) . (i + 1) = W . (m + i) & m + i in dom W )
hence (W .cut (m,n)) . (i + 1) = W . (m + i) by ; :: thesis: m + i in dom W
m + i < n + 1 by ;
then m + i <= n by NAT_1:13;
then A7: m + i <= len W by ;
1 <= m + i by ;
hence m + i in dom W by ; :: thesis: verum