let G be _Graph; :: thesis: for W being Walk of G

for m, n being Element of NAT st W is Trail-like holds

W .cut (m,n) is Trail-like

let W be Walk of G; :: thesis: for m, n being Element of NAT st W is Trail-like holds

W .cut (m,n) is Trail-like

let m, n be Element of NAT ; :: thesis: ( W is Trail-like implies W .cut (m,n) is Trail-like )

assume A1: W is Trail-like ; :: thesis: W .cut (m,n) is Trail-like

for m, n being Element of NAT st W is Trail-like holds

W .cut (m,n) is Trail-like

let W be Walk of G; :: thesis: for m, n being Element of NAT st W is Trail-like holds

W .cut (m,n) is Trail-like

let m, n be Element of NAT ; :: thesis: ( W is Trail-like implies W .cut (m,n) is Trail-like )

assume A1: W is Trail-like ; :: thesis: W .cut (m,n) is Trail-like

now :: thesis: W .cut (m,n) is Trail-like end;

hence
W .cut (m,n) is Trail-like
; :: thesis: verumper cases
( ( m is odd & n is odd & m <= n & n <= len W ) or not m is odd or not n is odd or not m <= n or not n <= len W )
;

end;

suppose A2:
( m is odd & n is odd & m <= n & n <= len W )
; :: thesis: W .cut (m,n) is Trail-like

end;

now :: thesis: for x, y being even Element of NAT st 1 <= x & x < y & y <= len (W .cut (m,n)) holds

(W .cut (m,n)) . x <> (W .cut (m,n)) . y

hence
W .cut (m,n) is Trail-like
by Lm57; :: thesis: verum(W .cut (m,n)) . x <> (W .cut (m,n)) . y

reconsider m9 = m as odd Element of NAT by A2;

let x, y be even Element of NAT ; :: thesis: ( 1 <= x & x < y & y <= len (W .cut (m,n)) implies (W .cut (m,n)) . x <> (W .cut (m,n)) . y )

assume that

A3: 1 <= x and

A4: x < y and

A5: y <= len (W .cut (m,n)) ; :: thesis: (W .cut (m,n)) . x <> (W .cut (m,n)) . y

reconsider xaa1 = x - 1 as odd Element of NAT by A3, INT_1:5;

reconsider yaa1 = y - 1 as odd Element of NAT by A3, A4, INT_1:5, XXREAL_0:2;

x - 1 < y - 1 by A4, XREAL_1:14;

then A6: xaa1 + m < yaa1 + m by XREAL_1:8;

x <= len (W .cut (m,n)) by A4, A5, XXREAL_0:2;

then x - 1 < (len (W .cut (m,n))) - 0 by XREAL_1:15;

then A7: (W .cut (m,n)) . (xaa1 + 1) = W . (m + xaa1) by A2, Lm15;

A8: y - 1 < (len (W .cut (m,n))) - 0 by A5, XREAL_1:15;

then A9: (W .cut (m,n)) . (yaa1 + 1) = W . (m + yaa1) by A2, Lm15;

m + yaa1 in dom W by A2, A8, Lm15;

then A10: m + yaa1 <= len W by FINSEQ_3:25;

1 <= m + xaa1 by ABIAN:12, NAT_1:12;

then W . (m9 + xaa1) <> W . (m9 + yaa1) by A1, A10, A6, Lm57;

hence (W .cut (m,n)) . x <> (W .cut (m,n)) . y by A7, A9; :: thesis: verum

end;let x, y be even Element of NAT ; :: thesis: ( 1 <= x & x < y & y <= len (W .cut (m,n)) implies (W .cut (m,n)) . x <> (W .cut (m,n)) . y )

assume that

A3: 1 <= x and

A4: x < y and

A5: y <= len (W .cut (m,n)) ; :: thesis: (W .cut (m,n)) . x <> (W .cut (m,n)) . y

reconsider xaa1 = x - 1 as odd Element of NAT by A3, INT_1:5;

reconsider yaa1 = y - 1 as odd Element of NAT by A3, A4, INT_1:5, XXREAL_0:2;

x - 1 < y - 1 by A4, XREAL_1:14;

then A6: xaa1 + m < yaa1 + m by XREAL_1:8;

x <= len (W .cut (m,n)) by A4, A5, XXREAL_0:2;

then x - 1 < (len (W .cut (m,n))) - 0 by XREAL_1:15;

then A7: (W .cut (m,n)) . (xaa1 + 1) = W . (m + xaa1) by A2, Lm15;

A8: y - 1 < (len (W .cut (m,n))) - 0 by A5, XREAL_1:15;

then A9: (W .cut (m,n)) . (yaa1 + 1) = W . (m + yaa1) by A2, Lm15;

m + yaa1 in dom W by A2, A8, Lm15;

then A10: m + yaa1 <= len W by FINSEQ_3:25;

1 <= m + xaa1 by ABIAN:12, NAT_1:12;

then W . (m9 + xaa1) <> W . (m9 + yaa1) by A1, A10, A6, Lm57;

hence (W .cut (m,n)) . x <> (W .cut (m,n)) . y by A7, A9; :: thesis: verum

suppose
( not m is odd or not n is odd or not m <= n or not n <= len W )
; :: thesis: W .cut (m,n) is Trail-like

end;

end;