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 A1, A2, Def11;
hence A5: (len (W .cut (m,n))) + m = n + 1 by A1, A2, A3, FINSEQ_6:def 4; :: 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 A1, A2, A4, A3, FINSEQ_6:def 4; :: thesis: m + i in dom W
m + i < n + 1 by A5, A6, XREAL_1:8;
then m + i <= n by NAT_1:13;
then A7: m + i <= len W by A2, XXREAL_0:2;
1 <= m + i by ABIAN:12, NAT_1:12;
hence m + i in dom W by A7, FINSEQ_3:25; :: thesis: verum