let G be _Graph; :: thesis: for W being Walk of G
for m, n being odd Element of NAT
for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut m,n) holds
( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
let W be Walk of G; :: thesis: for m, n being odd Element of NAT
for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut m,n) holds
( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
let m, n be odd Element of NAT ; :: thesis: for i being Element of NAT st m <= n & n <= len W & i in dom (W .cut m,n) holds
( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
let i be Element of NAT ; :: thesis: ( m <= n & n <= len W & i in dom (W .cut m,n) implies ( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) )
assume A1: ( m <= n & n <= len W & i in dom (W .cut m,n) ) ; :: thesis: ( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
then A2: ( 1 <= i & i <= len (W .cut m,n) ) by FINSEQ_3:27;
then reconsider iaa1 = i - 1 as Element of NAT by INT_1:18;
A3: iaa1 < (len (W .cut m,n)) - 0 by A2, XREAL_1:17;
iaa1 + 1 = i ;
then ( (W .cut m,n) . i = W . (m + iaa1) & m + iaa1 in dom W ) by A1, A3, Lm15;
hence ( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) ; :: thesis: verum