let G be _Graph; :: thesis: for W being Walk of G
for m, n being Element of NAT st W is Path-like holds
W .cut m,n is Path-like
let W be Walk of G; :: thesis: for m, n being Element of NAT st W is Path-like holds
W .cut m,n is Path-like
let m, n be Element of NAT ; :: thesis: ( W is Path-like implies W .cut m,n is Path-like )
assume A1: W is Path-like ; :: thesis: W .cut m,n is Path-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 Path-like

then reconsider m' = m as odd Element of NAT ;

now

W is Trail-like by A1, Def28;
hence W .cut m,n is Trail-like by Lm59; :: thesis: for x, y being odd Element of NAT st x < y & y <= len (W .cut m,n) & (W .cut m,n) . x = (W .cut m,n) . y holds
( x = 1 & y = len (W .cut m,n) )
let x, y be odd Element of NAT ; :: thesis: ( x < y & y <= len (W .cut m,n) & (W .cut m,n) . x = (W .cut m,n) . y implies ( x = 1 & y = len (W .cut m,n) ) )
assume A3: ( x < y & y <= len (W .cut m,n) & (W .cut m,n) . x = (W .cut m,n) . y ) ; :: thesis: ( x = 1 & y = len (W .cut m,n) )
reconsider xaa1 = x - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
reconsider yaa1 = y - 1 as even Element of NAT by HEYTING3:1, INT_1:18;
x <= len (W .cut m,n) by A3, XXREAL_0:2;
then x - 1 < (len (W .cut m,n)) - 0 by XREAL_1:17;
then A4: ( (W .cut m,n) . (xaa1 + 1) = W . (m + xaa1) & m + xaa1 in dom W ) by A2, Lm15;
y - 1 < (len (W .cut m,n)) - 0 by A3, XREAL_1:17;
then A5: ( (W .cut m,n) . (yaa1 + 1) = W . (m + yaa1) & m + yaa1 in dom W ) by A2, Lm15;
x - 1 < y - 1 by A3, XREAL_1:16;
then A6: xaa1 + m < yaa1 + m by XREAL_1:10;
A7: ( 1 <= m' + xaa1 & m' + yaa1 <= len W ) by A4, A5, FINSEQ_3:27;
then A8: ( m' + xaa1 = 1 & m' + yaa1 = len W ) by A1, A3, A4, A5, A6, Def28;

A9: now

assume xaa1 <> 0 ; :: thesis: contradiction
then ( 0 < xaa1 & m >= 1 ) by A2, HEYTING3:1;
then 1 + 0 < m + xaa1 by XREAL_1:10;
hence contradiction by A1, A3, A4, A5, A6, A7, Def28; :: thesis: verum

end;

hence x = 1 ; :: thesis: y = len (W .cut m,n)
(m + 1) - 1 = 1 by A1, A3, A4, A5, A6, A7, A9, Def28;
then (len (W .cut m,n)) + 1 = n + 1 by A2, Lm15;
hence y = len (W .cut m,n) by A2, A3, A8, A9, XXREAL_0:1; :: thesis: verum

end;

hence W .cut m,n is Path-like by Def28; :: 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 Path-like

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

end;

end;

end;

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