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

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 :: thesis: W .cut (m,n) is Path-like end;

hence
W .cut (m,n) is Path-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 Path-like

then reconsider m9 = m as odd Element of NAT ;

end;now :: thesis: ( W .cut (m,n) is Trail-like & ( 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)) ) ) )

hence
W .cut (m,n) is Path-like
; :: thesis: verum( x = 1 & y = len (W .cut (m,n)) ) ) )

W is Trail-like
by A1;

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 that

A3: x < y and

A4: y <= len (W .cut (m,n)) and

A5: (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 ABIAN:12, INT_1:5;

reconsider yaa1 = y - 1 as even Element of NAT by ABIAN:12, INT_1:5;

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

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

x <= len (W .cut (m,n)) by A3, A4, 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 A4, 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: m9 + yaa1 <= len W by FINSEQ_3:25;

then A11: m9 + yaa1 = len W by A1, A5, A7, A9, A6;

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

thus x = 1 by A12; :: thesis: y = len (W .cut (m,n))

m9 + xaa1 = 1 by A1, A5, A7, A9, A6, A10;

hence y = len (W .cut (m,n)) by A2, A4, A11, A12, A14, XXREAL_0:1; :: thesis: verum

end;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 that

A3: x < y and

A4: y <= len (W .cut (m,n)) and

A5: (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 ABIAN:12, INT_1:5;

reconsider yaa1 = y - 1 as even Element of NAT by ABIAN:12, INT_1:5;

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

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

x <= len (W .cut (m,n)) by A3, A4, 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 A4, 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: m9 + yaa1 <= len W by FINSEQ_3:25;

then A11: m9 + yaa1 = len W by A1, A5, A7, A9, A6;

A12: now :: thesis: not xaa1 <> 0

then
(m + 1) - 1 = 1
by A1, A5, A7, A9, A6, A10;assume A13:
xaa1 <> 0
; :: thesis: contradiction

m >= 1 by A2, ABIAN:12;

then 1 + 0 < m + xaa1 by A13, XREAL_1:8;

hence contradiction by A1, A5, A7, A9, A6, A10; :: thesis: verum

end;m >= 1 by A2, ABIAN:12;

then 1 + 0 < m + xaa1 by A13, XREAL_1:8;

hence contradiction by A1, A5, A7, A9, A6, A10; :: thesis: verum

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

thus x = 1 by A12; :: thesis: y = len (W .cut (m,n))

m9 + xaa1 = 1 by A1, A5, A7, A9, A6, A10;

hence y = len (W .cut (m,n)) by A2, A4, A11, A12, A14, XXREAL_0:1; :: thesis: verum