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 that
A1: m <= n and
A2: n <= len W and
A3: i in dom (W .cut (m,n)) ; :: thesis: ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
1 <= i by A3, FINSEQ_3:25;
then reconsider iaa1 = i - 1 as Element of NAT by INT_1:5;
i <= len (W .cut (m,n)) by A3, FINSEQ_3:25;
then A4: iaa1 < (len (W .cut (m,n))) - 0 by XREAL_1:15;
iaa1 + 1 = i ;
then (W .cut (m,n)) . i = W . (m + iaa1) by A1, A2, A4, Lm15;
hence ( (W .cut (m,n)) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W ) by A1, A2, A4, Lm15; :: thesis: verum