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