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 HEYTING3:1;
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, GRAPH_2:def 1; :: 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, GRAPH_2:def 1; :: thesis: m + i in dom W
m + i < n + 1 by A5, A6, XREAL_1:10;
then m + i <= n by NAT_1:13;
then A7: m + i <= len W by A2, XXREAL_0:2;
1 <= m + i by HEYTING3:1, NAT_1:12;
hence m + i in dom W by A7, FINSEQ_3:27; :: thesis: verum