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

now

per cases ( ( not m is even & not n is even & m <= n & n <= len W ) or m is even or n is even or not m <= n or not n <= len W ) ;

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

now

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:18;
reconsider yaa1 = y - 1 as odd Element of NAT by A3, A4, INT_1:18, XXREAL_0:2;
x - 1 < y - 1 by A4, XREAL_1:16;
then A6: xaa1 + m < yaa1 + m by XREAL_1:10;
x <= len (W .cut m,n) by A4, A5, XXREAL_0:2;
then x - 1 < (len (W .cut m,n)) - 0 by XREAL_1:17;
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:17;
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:27;
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;

hence W .cut m,n is Trail-like by Lm57; :: thesis: verum

end;

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

hence W .cut m,n is Trail-like by A1, Def11; :: thesis: verum

end;

end;

end;

hence W .cut m,n is Trail-like ; :: thesis: verum